coe_mk — Mathlib

English

An orthonormal family whose span is dense gives a Hilbert basis via the mk construction.

Русский

Ортонормированная семья, чья линейная оболочка плотна, образует Гильбертову базу через конструкцию mk.

LaTeX

$$$ HilbertBasis.mk hv hsp $$$

Lean4

@[simp]
protected theorem coe_mk (hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure) : ⇑(HilbertBasis.mk hv hsp) = v := by
  classical apply funext <| Orthonormal.linearIsometryEquiv_symm_apply_single_one hv hsp

Похожие утверждения