theorem isClosed_sup_of_isClosed_of_finiteDimensional_right {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {A B : Submodule ℝ H} (hA : IsClosed ↑A) [FiniteDimensional ℝ ↥B] : IsClosed ↑(A ⊔ B)

If A is closed and B is finite-dimensional, then A ⊔ B is closed.

theorem isClosed_sup_of_isClosed_of_finiteDimensional_orthogonal_right {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {A B : Submodule ℝ H} (hA : IsClosed ↑A) [FiniteDimensional ℝ ↥Aᗮ] : IsClosed ↑(B ⊔ A)

If A is closed and Aᗮ is finite-dimensional, then B ⊔ A is closed.

theorem isClosed_sup_of_isClosed_of_finiteDimensional_or_finiteDimensional_orthogonal {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {U V : Submodule ℝ H} (hU : IsClosed ↑U) (hV : IsClosed ↑V) (hfinite : FiniteDimensional ℝ ↥V ∨ FiniteDimensional ℝ ↥Vᗮ) : IsClosed ↑(U ⊔ V)

Fact 2.28: if U and V are closed linear subspaces of a real Hilbert space and V is finite-dimensional or has finite codimension in the sense that Vᗮ is finite-dimensional, then their sum U ⊔ V is closed.