English
If α is a CompleteAtomicBooleanAlgebra, then α is Atomistic.
Русский
Если α—полная атомарная булева алгебра, то она атомистична.
LaTeX
$$$[\\text{CompleteAtomicBooleanAlgebra}(\\alpha)] \\Rightarrow \\mathrm{IsAtomistic}(\\alpha)$$$
Lean4
instance {α} [CompleteAtomicBooleanAlgebra α] : IsAtomistic α :=
CompleteLattice.isAtomistic_iff.2 fun b ↦ by
inhabit α
refine ⟨{a | IsAtom a ∧ a ≤ b}, ?_, fun a ha => ha.1⟩
refine le_antisymm ?_ (sSup_le fun c hc => hc.2)
have : (⨅ c : α, ⨆ x, b ⊓ cond x c (cᶜ)) = b := by simp [iSup_bool_eq]
rw [← this]; clear this
simp_rw [iInf_iSup_eq, iSup_le_iff]; intro g
if h : (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥ then simp [h]
else
refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩; clear h
have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right)
revert this
nontriviality α
cases g c <;> simp
