linearProjOfClosedCompl — Mathlib

English

Projection onto a closed submodule along a closed complement is a bounded linear map.

Русский

Проекция на замкнутое подподпространство вдоль замкнутого дополнения — ограниченная линейная карта.

LaTeX

$$$$ \pi: E \to p \text{ linear, bounded} $$$$

Lean4

/-- Projection to a closed submodule along a closed complement. -/
def linearProjOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E)) (hq : IsClosed (q : Set E)) : E →L[𝕜] p :=
  ContinuousLinearMap.fst 𝕜 p q ∘L ↑(prodEquivOfClosedCompl p q h hp hq).symm

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