complementedLattice_of_sSup_atoms_eq_top

English

If atoms join to the top, there exists an independent set of atoms whose sSup is top and each element is an atom.

Русский

Если свойства атомов дают верх, существует независимый набор атомов с sSup = верх и каждый элемент — атом.

LaTeX

$$$ \text{Exists } s \text{ with } sSupIndep s \land sSup s = \top \land \forall a \in s, IsAtom a $$$

Lean4

/-- See [Theorem 6.6][calugareanu]. -/
theorem complementedLattice_of_sSup_atoms_eq_top (h : sSup {a : α | IsAtom a} = ⊤) : ComplementedLattice α where
  exists_isCompl
    b :=
    let ⟨s, _, hcompl, _⟩ := exists_sSupIndep_isCompl_sSup_atoms (by simpa) b
    ⟨sSup s, hcompl⟩

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