hasOrthogonalProjection_range — Mathlib

English

If p is idempotent on a complete space, then range p has an orthogonal projection.

Русский

Если p является идемпотентной на полному пространстве, то образ p имеет ортогональную проекцию.

LaTeX

$$$ [\text{CompleteSpace } E] \Rightarrow (\text{IsIdempotentElem } p) \Rightarrow \ \mathrm{range}(p) \text{HasOrthogonalProjection}$$$

Lean4

theorem _root_.ContinuousLinearMap.IsIdempotentElem.hasOrthogonalProjection_range [CompleteSpace E] {p : E →L[𝕜] E}
    (hp : IsIdempotentElem p) : (LinearMap.range p).HasOrthogonalProjection :=
  have := hp.isClosed_range.completeSpace_coe
  .ofCompleteSpace _

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