toColex_ofColex — Mathlib

English

The two encoding maps of Colex are inverses on finite sets: applying ofColex to a finite set s and then toColex again returns s, i.e., toColex (ofColex s) = s for all s in Finset.Colex α.

Русский

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

LaTeX

$$$\forall s \in Finset.Colex(\alpha):\; toColex (ofColex s) = s$$$

Lean4

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

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