singleton_lt_singleton

Mathlib.Combinatorics.Colex

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

← MathLib Explorer

English

For any a,b, {a} < {b} if and only if a < b in the base order.

Русский

Для любых a,b: {a} < {b} тогда и только тогда, когда a < b в базовом порядке.

LaTeX

$$$$ \\operatorname{toColex}({a}) < \\operatorname{toColex}({b}) \\iff a < b $$$$

Lean4

/-- Colex is an extension of the base order. -/
theorem singleton_lt_singleton : (toColex ({ a } : Finset α)) < toColex { b } ↔ a < b := by simp [toColex_lt_singleton]

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

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

Разделы

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

Аффилиация

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