projection_eq_self_sub_projection

English

Let p and q be complementary subspaces of E (i.e., E = p ⊕ q). Then the projection to p along q and the projection to q along p satisfy P_q^p(x) = x − P_p^q(x) for all x ∈ E.

Русский

Пусть p и q — дополнительные (комплементные) подпространства в E, то есть E = p ⊕ q. Тогда проекция на p вдоль q и проекция на q вдоль p удовлетворяют тождеству P_q^p(x) = x − P_p^q(x) для всех x ∈ E.

LaTeX

$$$P_q^{p}(x) = x - P_p^{q}(x),$ where $P_p^{q}$ is the projection onto $p$ along $q$.$$

Lean4

theorem projection_eq_self_sub_projection (hpq : IsCompl p q) (x : E) : hpq.symm.projection x = x - hpq.projection x :=
  by rw [eq_sub_iff_add_eq, projection_add_projection_eq_self]

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