k : Type u_2
V : Type u_4
P : Type u_1
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
ι : Type ?u.331791
V₂ : Type u_5
P₂ : Type u_3
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P
e : P ≃ᵃ[k] P₂
this : ↑e ∘ Subtype.val = Subtype.val ∘ ↑(Equiv.image (↑e) s)
⊢ AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val
k : Type u_2
V : Type u_4
P : Type u_1
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
ι : Type ?u.331791
V₂ : Type u_5
P₂ : Type u_3
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P
e : P ≃ᵃ[k] P₂
⊢ AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val
have : e ∘ ((↑) : s → P) = ((↑) : e '' s → P₂) ∘ (e : P ≃ P₂).image s := rfl
no goals
k : Type u_2
V : Type u_4
P : Type u_1
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AffineSpace V P
ι : Type ?u.331791
V₂ : Type u_5
P₂ : Type u_3
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
s : Set P
e : P ≃ᵃ[k] P₂
this : ↑e ∘ Subtype.val = Subtype.val ∘ ↑(Equiv.image (↑e) s)
⊢ AffineIndependent k Subtype.val ↔ AffineIndependent k Subtype.val
rw [← e.affineIndependent_iff, this, affineIndependent_equiv]