ofColex_inj — Mathlib

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

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