𝕜 : Type u_2
E : Type u_1
F : Type ?u.771484
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h_mem : v ∈ K ⊔ Kᗮ
⊢ ∃ y, y ∈ K ∧ ∃ z, z ∈ Kᗮ ∧ v = y + z
𝕜 : Type u_2
E : Type u_1
F : Type ?u.771484
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ ∃ y, y ∈ K ∧ ∃ z, z ∈ Kᗮ ∧ v = y + z
have h_mem : v ∈ K ⊔ Kᗮ := by simp [Submodule.sup_orthogonal_of_completeSpace]
case intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.771484
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h_mem : v ∈ K ⊔ Kᗮ
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hyz : y + z = v
⊢ ∃ y, y ∈ K ∧ ∃ z, z ∈ Kᗮ ∧ v = y + z
𝕜 : Type u_2
E : Type u_1
F : Type ?u.771484
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h_mem : v ∈ K ⊔ Kᗮ
⊢ ∃ y, y ∈ K ∧ ∃ z, z ∈ Kᗮ ∧ v = y + z
obtain ⟨y, hy, z, hz, hyz⟩ := Submodule.mem_sup.mp h_mem
no goals
case intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.771484
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
h_mem : v ∈ K ⊔ Kᗮ
y : E
hy : y ∈ K
z : E
hz : z ∈ Kᗮ
hyz : y + z = v
⊢ ∃ y, y ∈ K ∧ ∃ z, z ∈ Kᗮ ∧ v = y + z
exact ⟨y, hy, z, hz, hyz.symm⟩
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.771484
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ K }
v : E
⊢ v ∈ K ⊔ Kᗮ
simp [Submodule.sup_orthogonal_of_completeSpace]