no goals
α : Type u_1
β : Type ?u.18041
inst✝ : CompleteLattice α
h : IsAtomistic αᵒᵈ
b : α
⊢ ∃ s, b = sInf s ∧ ∀ (a : α), a ∈ s → IsCoatom a
apply h.eq_sSup_atoms
no goals
α : Type u_1
β : Type ?u.18041
inst✝ : CompleteLattice α
h : IsCoatomistic α
b : αᵒᵈ
⊢ ∃ s, b = sSup s ∧ ∀ (a : αᵒᵈ), a ∈ s → IsAtom a
apply h.eq_sInf_coatoms