mkOfOrthogonalEqBot — Mathlib

English

If the orthogonal complement is trivial, an orthonormal family is a Hilbert basis.

Русский

Если ортогональное дополнение тривиально, орто-нормальная семья является Гильбертовой базой.

LaTeX

$$$ HilbertBasis.mkOfOrthogonalEqBot(hsp) : HilbertBasis ι 𝕜 E $$$

Lean4

/-- An orthonormal family of vectors whose span has trivial orthogonal complement is a Hilbert
basis. -/
protected def mkOfOrthogonalEqBot (hsp : (span 𝕜 (Set.range v))ᗮ = ⊥) : HilbertBasis ι 𝕜 E :=
  HilbertBasis.mk hv (by rw [← orthogonal_orthogonal_eq_closure, ← eq_top_iff, orthogonal_eq_top_iff, hsp])

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