exists_sSupIndep_of_sSup_atoms_eq_top

English

In an atomic modular lattice, there exists an s such that sSupIndep s, IsCompl b (sSup s) and every a ∈ s is an atom.

Русский

В атомной модульной решётке существует набор атомов s, удовлетворяющий: sSupIndep s, IsCompl b (sSup s), и каждый элемент множества — атом.

LaTeX

$$$ \exists s, sSupIndep s \land IsCompl b (sSup s) \land \forall a \in s, IsAtom a $$$

Lean4

theorem exists_sSupIndep_of_sSup_atoms_eq_top (h : sSup {a : α | IsAtom a} = ⊤) :
    ∃ s : Set α, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ ⦃a⦄, a ∈ s → IsAtom a :=
  exists_sSupIndep_of_sSup_atoms ⊤ (by simpa)

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