toColex_injective — Mathlib

English

The map toColex is injective: s ≠ t implies toColex s ≠ toColex t; equivalently, if toColex s = toColex t then s = t.

Русский

Карта toColex инъективна: если s ≠ t, то toColex s ≠ toColex t (или равносильное утверждение: toColex s = toColex t ⇒ s = t).

LaTeX

$$$\forall s,t:\ Finset(\alpha),\ toColex s = toColex t \Rightarrow s = t$$$

Lean4

@[deprecated toColex_inj (since := "2025-08-28")]
theorem toColex_injective : Injective (Finset.Colex.toColex : Finset α → Finset.Colex α) := fun _ _ ↦
  Finset.toColex_inj.1

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