instOrthogonalCompleteSpace — Mathlib

English

If E is a complete normed space, then the orthogonal complement K^⊥ of any subspace K is a complete subspace of E.

Русский

Если пространство E полноценно нормировано, то ортогональное дополнение K^⊥ любого подпространства K является полным подпространством E.

LaTeX

$$$\text{CompleteSpace}(K^\perp)$$$

Lean4

/-- In a complete space, the orthogonal complement of any submodule `K` is complete. -/
instance instOrthogonalCompleteSpace [CompleteSpace E] : CompleteSpace Kᗮ :=
  K.isClosed_orthogonal.completeSpace_coe

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