English
For an orthogonal family V, DirectSum.IsInternal V is equivalent to the orthogonal complement of its sup is zero.
Русский
Для ортогональной системы V условие DirectSum.IsInternal эквивалентно нулю ортогонального дополнения суммирования iSup V.
LaTeX
$$$\\text{DirectSum.IsInternal } V \\iff (iSup 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 [DecidableEq ι] [FiniteDimensional 𝕜 E] {V : ι → Submodule 𝕜 E}
(hV : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) : DirectSum.IsInternal V ↔ (iSup V)ᗮ = ⊥ :=
haveI := FiniteDimensional.proper_rclike 𝕜 (↥(iSup V))
hV.isInternal_iff_of_isComplete (completeSpace_coe_iff_isComplete.mp inferInstance)
