sSup_atoms_le_eq — Mathlib

English

In an atomistic complete lattice, for any b, the supremum of atoms a ≤ b equals b.

Русский

В атомистичной полной решетке для любого b наибольшая верхняя граница атомов a ≤ b равна b.

LaTeX

$$$IsLUB\\{a : \\alpha \\mid IsAtom a \\land a \\le b\\} b$$$

Lean4

@[simp]
theorem sSup_atoms_le_eq {α} [CompleteLattice α] [IsAtomistic α] (b : α) : sSup {a : α | IsAtom a ∧ a ≤ b} = b :=
  (isLUB_atoms_le b).sSup_eq

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