toColex_inj — Mathlib

English

The map s ↦ toColex s from Finset α to Finset.Colex α is injective: if toColex s = toColex t then s = t.

Русский

Отображение s ↦ toColex s из Finset α в Finset.Colex α инъективно: если 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")]
protected theorem toColex_inj {s t : Finset α} : Finset.Colex.toColex s = Finset.Colex.toColex t ↔ s = t := by simp

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