English
An orthogonal family of subspaces provides an internal direct sum if and only if the orthogonal complement of the span is trivial.
Русский
Ортогональная система подпространств образует внутреннее разложение пространства по прямой сумме тогда и только тогда, когда ортогональное дополнение порождающего пространства тривиально.
LaTeX
$$$\\text{DirectSum.IsInternal } V \\iff (\\operatorname{span} V)^{\\perp} = \\{0\\}$$$
Lean4
/-- An orthogonal family of subspaces of `E` satisfies `DirectSum.IsInternal` (that is,
they provide an internal direct sum decomposition of `E`) if and only if their span has trivial
orthogonal complement. -/
theorem isInternal_iff_of_isComplete [DecidableEq ι] {V : ι → Submodule 𝕜 E}
(hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) (hc : IsComplete (↑(iSup V) : Set E)) :
DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥ :=
by
haveI : CompleteSpace (↥(iSup V)) := hc.completeSpace_coe
simp only [DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, hV.independent, true_and,
orthogonal_eq_bot_iff]
