case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.131964
G : Type ?u.131967
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q✝ : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
⊢ Submodule.ClosedComplemented p
𝕜 : Type u_1
E : Type u_2
F : Type ?u.131964
G : Type ?u.131967
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
⊢ Submodule.ClosedComplemented p
obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.131964
G : Type ?u.131967
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q✝ : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
this : FiniteDimensional 𝕜 { x // x ∈ q }
⊢ Submodule.ClosedComplemented p
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.131964
G : Type ?u.131967
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q✝ : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
⊢ Submodule.ClosedComplemented p
haveI : FiniteDimensional 𝕜 q := (p.quotientEquivOfIsCompl q hq).finiteDimensional
no goals
case intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.131964
G : Type ?u.131967
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : CompleteSpace E
p q✝ : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
this : FiniteDimensional 𝕜 { x // x ∈ q }
⊢ Submodule.ClosedComplemented p
exact closedComplemented_of_closed_compl hq hp q.closed_of_finiteDimensional