instIsAtomistic

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#IsSimpleOrder.instIsAtomistic

English

A simple order is atomistic: the lattice is generated by its atoms.

Русский

Простой порядок атомистичен: решётка порождается своими атомами.

LaTeX

$$$\text{IsAtomistic}(\alpha)$$$

Lean4

instance (priority := 100) : IsAtomistic α where
  isLUB_atoms b := (eq_bot_or_eq_top b).elim (fun h ↦ ⟨∅, by simp [h]⟩) (fun h ↦ ⟨{⊤}, by simp [h]⟩)

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

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

Разделы

Аффилиация

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