k : Type u_5
V₁ : Type u_3
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.576335
P₃ : Type ?u.576338
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ↑f
⊢ ↑(AffineSubspace.map f ⊤) = ↑⊤
k : Type u_5
V₁ : Type u_3
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.576335
P₃ : Type ?u.576338
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ↑f
⊢ AffineSubspace.map f ⊤ = ⊤
rw [← AffineSubspace.ext_iff]
no goals
k : Type u_5
V₁ : Type u_3
P₁ : Type u_1
V₂ : Type u_4
P₂ : Type u_2
V₃ : Type ?u.576335
P₃ : Type ?u.576338
inst✝⁹ : Ring k
inst✝⁸ : AddCommGroup V₁
inst✝⁷ : Module k V₁
inst✝⁶ : AffineSpace V₁ P₁
inst✝⁵ : AddCommGroup V₂
inst✝⁴ : Module k V₂
inst✝³ : AffineSpace V₂ P₂
inst✝² : AddCommGroup V₃
inst✝¹ : Module k V₃
inst✝ : AffineSpace V₃ P₃
f : P₁ →ᵃ[k] P₂
hf : Function.Surjective ↑f
⊢ ↑(AffineSubspace.map f ⊤) = ↑⊤
exact image_univ_of_surjective hf