ofIsCompl_subtype_zero_eq — Mathlib

English

The projection built from IsCompl equals the projection to the subtype on p when the other part is zero.

Русский

Проекция, построенная из IsCompl, совпадает с проекцией на подпроство p при нулевой другой части.

LaTeX

$$$\mathrm{ofIsCompl\ hpq\ p.subtype\ 0 = hpq.projection}.$$$

Lean4

theorem ofIsCompl_subtype_zero_eq (hpq : IsCompl p q) : ofIsCompl hpq p.subtype 0 = hpq.projection := by
  simp [ofIsCompl_eq_add, IsCompl.projection]

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