mem_range_iff — Mathlib

English

Given an idempotent p, x ∈ range p iff p x = x.

Русский

Для идемпотентного p: x в образе p тогда и только тогда, когда p x = x.

LaTeX

$$x ∈ \operatorname{range} p \iff p x = x$$

Lean4

/-- Given an idempotent linear operator `p`, we have
`x ∈ range p` if and only if `p(x) = x` for all `x`. -/
theorem mem_range_iff {p : M →ₗ[S] M} (hp : IsIdempotentElem p) {x : M} : x ∈ range p ↔ p x = x :=
  hp.isProj_range.mem_iff_map_id

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