k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
⊢ affineSpan k (↑e '' s) = ⊤ → affineSpan k s = ⊤
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
⊢ affineSpan k s = ⊤ ↔ affineSpan k (↑e '' s) = ⊤
refine' ⟨(e : P₁ →ᵃ[k] P₂).span_eq_top_of_surjective e.surjective, _⟩
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
⊢ affineSpan k s = ⊤
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
⊢ affineSpan k (↑e '' s) = ⊤ → affineSpan k s = ⊤
intro h
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
this : s = ↑(symm e) '' (↑e '' s)
⊢ affineSpan k s = ⊤
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
⊢ affineSpan k s = ⊤
have : s = e.symm '' (e '' s) := by rw [← image_comp]; simp
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
this : s = ↑(symm e) '' (↑e '' s)
⊢ affineSpan k (↑(symm e) '' (↑e '' s)) = ⊤
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
this : s = ↑(symm e) '' (↑e '' s)
⊢ affineSpan k s = ⊤
rw [this]
no goals
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
this : s = ↑(symm e) '' (↑e '' s)
⊢ affineSpan k (↑(symm e) '' (↑e '' s)) = ⊤
exact (e.symm : P₂ →ᵃ[k] P₁).span_eq_top_of_surjective e.symm.surjective h
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
⊢ s = ↑(symm e) ∘ ↑e '' s
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
⊢ s = ↑(symm e) '' (↑e '' s)
rw [← image_comp]
no goals
k : Type u_2
V₁ : Type u_4
P₁ : Type u_1
V₂ : Type u_5
P₂ : Type u_3
V₃ : Type ?u.582825
P₃ : Type ?u.582828
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₂
s : Set P₁
e : P₁ ≃ᵃ[k] P₂
h : affineSpan k (↑e '' s) = ⊤
⊢ s = ↑(symm e) ∘ ↑e '' s
simp