linearProjOfIsCompl_comp_subtype — Mathlib

English

The composition (linearProjOfIsCompl p q h) ∘ p.subtype equals the identity on p.

Русский

Составление (linearProjOfIsCompl p q h) ∘ p.subtype даёт тождественную отображение на p.

LaTeX

$$$\bigl(linearProjOfIsCompl p q h\bigr)\circ p.subtype = \mathrm{id}_p$$$

Lean4

theorem linearProjOfIsCompl_comp_subtype (h : IsCompl p q) :
    (linearProjOfIsCompl p q h).comp p.subtype = LinearMap.id :=
  LinearMap.ext <| linearProjOfIsCompl_apply_left h

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