ofColex_ne_ofColex — Mathlib

English

For s,t ∈ Finset.Colex α, Finset.Colex.ofColex s ≠ Finset.Colex.ofColex t iff s ≠ t.

Русский

Для s,t ∈ Finset.Colex α верно: Finset.Colex.ofColex s ≠ Finset.Colex.ofColex t эквивалентно s ≠ t.

LaTeX

$$$\forall s,t:\ Finset.Colex(\alpha),\ Finset.Colex.ofColex s \neq Finset.Colex.ofColex t \iff s \neq t$$$

Lean4

@[deprecated ofColex_inj (since := "2025-08-28")]
theorem ofColex_ne_ofColex {s t : Finset.Colex α} : Finset.Colex.ofColex s ≠ Finset.Colex.ofColex t ↔ s ≠ t := by
  simp [Finset.ofColex_inj]

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