Lcomplement — Mathlib

English

If P is an L-projection on X (i.e., a linear projection with the L-norm property), then 1 − P is also an L-projection on X.

Русский

Если P — L-проекция на X (линейная проекция с указанной L-нормой), то 1 − P также является L-проекцией на X.

LaTeX

$$If $P$ is an $L$-projection on $X$, then $1-P$ is an $L$-projection on $X$.$$

Lean4

theorem Lcomplement {P : M} (h : IsLprojection X P) : IsLprojection X (1 - P) :=
  ⟨h.proj.one_sub, fun x => by
    rw [add_comm, sub_sub_cancel]
    exact h.Lnorm x⟩

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