sSup_atoms_eq_top

Mathlib.Order.Atoms

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

English

In a complete lattice with atoms and a top, the supremum of all atoms equals the top element.

Русский

Если есть атомы и верхняя граница, то их супремум равен верху.

LaTeX

$$$IsLUB\\{a : \\alpha \\mid IsAtom a\\} \\top$$$

Lean4

@[simp]
theorem sSup_atoms_eq_top {α} [CompleteLattice α] [IsAtomistic α] : sSup {a : α | IsAtom a} = ⊤ :=
  isLUB_atoms_top.sSup_eq

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

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

Разделы

Аффилиация

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