of_isIdempotentElem — Mathlib

English

If e is idempotent, then the block [e, 1 − e] forms a complete orthogonal idempotents system.

Русский

Если e идемпотент, то блок [e, 1 − e] образует систему полных ортогональных идемпотентов.

LaTeX

$$$\\text{CompleteOrthogonalIdempotents}([e, 1 - e])$$$

Lean4

theorem of_isIdempotentElem {e : R} (he : IsIdempotentElem e) : CompleteOrthogonalIdempotents ![e, 1 - e] :=
  pair_iff.mpr ⟨he, rfl⟩

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