toColex_le_toColex_of_subset

Mathlib.Combinatorics.Colex

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

← MathLib Explorer

English

If s ⊆ t, then toColex s ≤ toColex t.

Русский

Если s ⊆ t, то toColex s ≤ toColex t.

LaTeX

$$$s \subseteq t \Rightarrow toColex s \le 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_le_toColex_of_subset (h : s ⊆ t) : toColex s ≤ toColex t :=
  toColex_mono h

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

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

Разделы

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

Аффилиация

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