toColex_ne_toColex

Mathlib.Combinatorics.Colex

URI: https://scilib.ai/kg/mathlib#Finset.toColex_ne_toColex

← MathLib Explorer

English

The negation form: toColex s ≠ toColex t if and only if s ≠ t.

Русский

Неравенство в Colex перекладывается так: toColex s ≠ toColex t эквивалентно s ≠ t.

LaTeX

$$$\, toColex s \neq toColex t \iff s \neq t$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru