English
A finite orthonormal family whose span has trivial orthogonal complement yields an orthonormal basis.
Русский
Конечная ортонормированная семейство, обладающее нулевым ортогональным дополнением к своему обобщению, образует ортонормированную базу.
LaTeX
$$$$ \\text{If } hon \\text{ is orthonormal and } (\\operatorname{span}(\\mathrm{range}(v)))^{\\perp} = \\{0\\}, \\quad \\mathrm{OrthonormalBasis.mkOfOrthogonalEqBot}(hon,hsp) \\text{ is an orthonormal basis of } E. $$$$
Lean4
/-- A finite orthonormal family of vectors whose span has trivial orthogonal complement is an
orthonormal basis. -/
protected def mkOfOrthogonalEqBot (hon : Orthonormal 𝕜 v) (hsp : (span 𝕜 (Set.range v))ᗮ = ⊥) :
OrthonormalBasis ι 𝕜 E :=
OrthonormalBasis.mk hon
(by
refine Eq.ge ?_
haveI : FiniteDimensional 𝕜 (span 𝕜 (range v)) := FiniteDimensional.span_of_finite 𝕜 (finite_range v)
haveI : CompleteSpace (span 𝕜 (range v)) := FiniteDimensional.complete 𝕜 _
rwa [orthogonal_eq_bot_iff] at hsp)
