mkInternal — Mathlib

English

Equivalence between the actual Hilbert sum construction and its reverse isometry description.

Русский

Эквивалентность между фактическим построением Гильбертовой суммы и описанием через обратную изомортику.

LaTeX

$$$ IsHilbertSum.mk\\, (V) = IsHilbertSum.linearIsometryEquiv \\circ IsHilbertSum.mk \\; $$$

Lean4

/-- This is `Orthonormal.isHilbertSum` in the case of actual inclusions from subspaces. -/
theorem mkInternal [∀ i, CompleteSpace <| F i] (hFortho : OrthogonalFamily 𝕜 (fun i => F i) fun i => (F i).subtypeₗᵢ)
    (hFtotal : ⊤ ≤ (⨆ i, F i).topologicalClosure) : IsHilbertSum 𝕜 (fun i => F i) fun i => (F i).subtypeₗᵢ :=
  IsHilbertSum.mk hFortho (by simpa [subtypeₗᵢ_toLinearMap, range_subtype] using hFtotal)

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