isAtom_top

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#isAtom_top

English

In a simple order, the top element is an atom.

Русский

В простом порядке вершина является атомом.

LaTeX

$$$\text{IsAtom}(\top)$$$

Lean4

theorem isAtom_top : IsAtom (⊤ : α) :=
  ⟨top_ne_bot, fun a ha => Or.resolve_right (eq_bot_or_eq_top a) (ne_of_lt ha)⟩

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

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

Разделы

Аффилиация

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