projection_add_projection_eq_self

English

The sum of the projections onto p and onto q along their complement equals the identity on E, i.e., hpq.projection x + hpq.symm.projection x = x.

Русский

Сумма проекций на p и на q вдоль их дополнения равна тождественному отображению на E: hpq.projection x + hpq.symm.projection x = x.

LaTeX

$$$hpq.projection(x) + hpq.symm.projection(x) = x$$$

Lean4

theorem projection_add_projection_eq_self (hpq : IsCompl p q) (x : E) : hpq.projection x + hpq.symm.projection x = x :=
  by
  dsimp only [IsCompl.projection, linearProjOfIsCompl]
  rw [← prodComm_trans_prodEquivOfIsCompl _ _ hpq]
  exact (prodEquivOfIsCompl _ _ hpq).apply_symm_apply x

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