range_eq_ker — Mathlib

English

For an idempotent endomorphism p, the image of p equals the kernel of I − p, where I is the identity on the space.

Русский

Для идемпотентного эндоморфизма p образ p равен ядру I − p, где I — тождественный оператор.

LaTeX

$$$ \operatorname{Im}(p) = \ker(I - p) $$$

Lean4

theorem range_eq_ker {E : Type*} [AddCommGroup E] [Module S E] {p : E →ₗ[S] E} (hp : IsIdempotentElem p) :
    LinearMap.range p = LinearMap.ker (1 - p) :=
  le_antisymm (LinearMap.range_le_ker_iff.mpr hp.one_sub_mul_self) fun x hx ↦
    ⟨x, by simpa [sub_eq_zero, eq_comm (a := x)] using hx⟩

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