toColex_mono

Mathlib.Combinatorics.Colex

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

← MathLib Explorer

English

A collection of simp-specialized equivalences for the Colex comparison.

Русский

Набор упрощённых эквивалентностей сравнения Colex.

LaTeX

$$$\text{simp}_{\text{Colex}}(s,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_mono : Monotone (@toColex (Finset α)) := fun _s _t hst _a has hat ↦ (hat <| hst has).elim

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

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

Разделы

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

Аффилиация

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