eq_sSup_atoms — Mathlib

English

For a complete lattice with atomistic structure, every element b can be written as the supremum of a set of atoms.

Русский

В атомистичной полной решетке каждый элемент равен супремусу некоторого множества атомов.

LaTeX

$$∃ s : Set α, b = sSup s ∧ ∀ a ∈ s, IsAtom a$$

Lean4

theorem eq_sSup_atoms {α} [CompleteLattice α] [IsAtomistic α] (b : α) : ∃ s : Set α, b = sSup s ∧ ∀ a ∈ s, IsAtom a :=
  CompleteLattice.isAtomistic_iff.1 ‹_› b

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