singleton_le_singleton — Mathlib

English

The Colex order between two singleton sets {a} and {b} is determined exactly by the base order: {a} ≤ {b} iff a ≤ b.

Русский

Порядок Коэкса между одиночными множествами {a} и {b} задаётся точно базовым порядком: {a} ≤ {b} эквивалентно a ≤ b.

LaTeX

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

Lean4

/-- Colex is an extension of the base order. -/
theorem singleton_le_singleton : (toColex ({ a } : Finset α)) ≤ toColex { b } ↔ a ≤ b := by
  simp [toColex_le_singleton, eq_comm]

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