English
The reverse map Finset.Colex.ofColex is injective, i.e., if ofColex s = ofColex t then s = t, for s,t in Finset.Colex α.
Русский
Обратное отображение Finset.Colex.ofColex инъективно: если ofColex s = ofColex t, то s = t, для s,t в Finset.Colex α.
LaTeX
$$$\forall s,t:\ Finset.Colex(\alpha),\ ofColex s = ofColex t \Rightarrow s = t$$$
Lean4
@[deprecated ofColex_inj (since := "2025-08-28")]
protected theorem ofColex_inj {s t : Finset.Colex α} : Finset.Colex.ofColex s = Finset.Colex.ofColex t ↔ s = t := by
cases s; cases t; simp