ofColex_injective — Mathlib

English

The map ofColex is injective: s.ofColex = t.ofColex implies s = t for Finset.Colex α.

Русский

Обратное отображение Colex инъективно: s.ofColex = t.ofColex ⇒ s = t.

LaTeX

$$$\forall s,t:\ Finset.Colex(\alpha),\ s.ofColex = t.ofColex \Rightarrow s = t$$$

Lean4

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

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