isAtomistic_of_sSup_eq_top — Mathlib

English

If hS: BooleanGenerators S and sSup S = ⊤, then α is atomistic.

Русский

Если hS: BooleanGenerators S и sSup S = ⊤, то α атомистично.

LaTeX

$$$ \text{BooleanGenerators}(S) \rightarrow (sSup S = \top) \rightarrow \text{IsAtomistic } α $$$

Lean4

theorem isAtomistic_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) : IsAtomistic α :=
  by
  refine CompleteLattice.isAtomistic_iff.2 fun a ↦ ?_
  obtain ⟨s, hs, hs'⟩ := hS.atomistic a (h ▸ le_top)
  exact ⟨s, hs', fun I hI ↦ hS.isAtom I (hs hI)⟩

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