eq_atoms_of_sSup_eq_top — Mathlib

English

If sSup S = ⊤, then S equals the set of atoms: S = {a | IsAtom a}.

Русский

Если sSup S = ⊤, то S = {a | IsAtom a}.

LaTeX

$$$ sSup S = \top \rightarrow S = \{a : α \mid IsAtom a\}$$$

Lean4

theorem eq_atoms_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) : S = {a : α | IsAtom a} :=
  by
  apply le_antisymm
  · exact hS.isAtom
  intro a ha
  obtain ⟨T, hT, rfl⟩ := hS.atomistic a (le_top.trans h.ge)
  exact hS.mem_of_isAtom_of_le_sSup_atoms _ ha (sSup_le_sSup hT)

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