projection_eq_self_iff — Mathlib

English

For complementary subspaces p and q of E and any x ∈ E, the projection of x to p along q equals x if and only if x ∈ p.

Русский

Пусть p и q — дополняющие подпространства E. Тогда для любого вектора x ∈ E проекция x на p вдоль q равна x тогда и только если x ∈ p.

LaTeX

$$$P_p^{q}(x) = x \quad\Longleftrightarrow\quad x \in p,$$$

Lean4

/-- The projection to `p` along `q` of `x` equals `x` if and only if `x ∈ p`. -/
@[simp]
theorem projection_eq_self_iff (hpq : IsCompl p q) (x : E) : hpq.projection x = x ↔ x ∈ p := by
  rw [eq_comm, ← sub_eq_zero, ← projection_eq_self_sub_projection, projection_apply_eq_zero_iff]

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