unique — Mathlib

English

If there is a unique index set I, then OrthogonalIdempotents e is equivalent to IsIdempotentElem (e default).

Русский

Если множество индексов единственно, то OrthogonalIdempotents e эквивалентно IsIdempotentElem (e по умолчанию).

LaTeX

$$OrthogonalIdempotents e ↔ IsIdempotentElem (e default)$$

Lean4

theorem unique [Unique I] : OrthogonalIdempotents e ↔ IsIdempotentElem (e default) := by
  simp only [orthogonalIdempotents_iff, Unique.forall_iff, Subsingleton.pairwise, and_true]

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