isAtomistic_iff — Mathlib

English

In a complete lattice, IsAtomistic is equivalent to every element being a sup of atoms.

Русский

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

LaTeX

$$nonrec theorem isAtomistic_iff {\\alpha} [CompleteLattice \\alpha] : IsAtomistic \\alpha \\iff \\forall b : \\alpha, \\exists s : Set \\alpha, b = sSup s ∧ \\forall a ∈ s, IsAtom a$$

Lean4

nonrec theorem isAtomistic_iff {α} [CompleteLattice α] :
    IsAtomistic α ↔ ∀ b : α, ∃ s : Set α, b = sSup s ∧ ∀ a ∈ s, IsAtom a := by
  simp_rw [isAtomistic_iff, isLUB_iff_sSup_eq, eq_comm]

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