toColex_lt_toColex_of_ssubset

Mathlib.Combinatorics.Colex

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

← MathLib Explorer

English

If s ⊂ t, then toColex s < toColex t.

Русский

Если s ⊂ t, то toColex s < toColex t.

LaTeX

$$$s \subset t \Rightarrow toColex s < toColex 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_lt_toColex_of_ssubset (h : s ⊂ t) : toColex s < toColex t :=
  toColex_strictMono h

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

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

Разделы

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

Аффилиация

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