toColex_strictMono

Mathlib.Combinatorics.Colex

URI: https://scilib.ai/kg/mathlib#Finset.Colex.toColex_strictMono

← MathLib Explorer

English

A simp lemma: toColex s ≠ toColex t ↔ s ≠ t.

Русский

Упрощённая лемма: toColex s ≠ toColex t ↔ s ≠ t.

LaTeX

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

Lean4

/-- If `s ⊂ t`, then `s < t` in the colex order. Note the converse does not hold, as inclusion does
not form a linear order. -/
theorem toColex_strictMono : StrictMono (@toColex (Finset α)) :=
  toColex_mono.strictMono_of_injective toColex.injective

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

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

Разделы

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

Аффилиация

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