English
If hon is an orthonormal family v indexed by ι and hsp asserts that the span of Range(v) is all of E, then the construction OrthonormalBasis.mk hon hsp defines an orthonormal basis of E.
Русский
Пусть v — ортонормированная система в E, индексированная ι, и пусть span(Range(v)) = E. Тогда конструкция OrthonormalBasis.mk hon hsp задаёт ортонормированную базу пространства E.
LaTeX
$$$$ \\text{If } hon \\text{ is orthonormal and } \\top \\le \\operatorname{span}_k(\\operatorname{Range}(v)), \\text{ then } \\mathrm{OrthonormalBasis.mk}(hon,hsp) \\text{ is an orthonormal basis of } E. $$$$
Lean4
/-- A finite orthonormal set that spans is an orthonormal basis -/
protected def mk (hon : Orthonormal 𝕜 v) (hsp : ⊤ ≤ Submodule.span 𝕜 (Set.range v)) : OrthonormalBasis ι 𝕜 E :=
(Basis.mk (Orthonormal.linearIndependent hon) hsp).toOrthonormalBasis (by rwa [Basis.coe_mk])
