ofColex_toColex — Mathlib

English

For any finite set s, applying toColex to a finite set s and then ofColex returns the original s, i.e., ofColex (toColex s) = s.

Русский

Для любого конечного множества s применяется toColex к s и затем возвращает s через ofColex: ofColex (toColex s) = s.

LaTeX

$$$\forall s:\ Finset(\alpha),\; ofColex (toColex s) = s$$$

Lean4

@[deprecated ofColex_toColex (since := "2025-08-28")]
protected theorem ofColex_toColex (s : Finset α) : Finset.Colex.ofColex (Finset.Colex.toColex s) = s :=
  rfl

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