toCompleteAtomicBooleanAlgebra — Mathlib

English

Every atomic complete Boolean algebra is completely atomic.

Русский

Каждая атомарная полная булева алгебра completely atomic.

LaTeX

$$$\\text{CompleteBooleanAlgebra}(\\alpha) \\wedge \\text{IsAtomic}(\\alpha) \\Rightarrow \\text{CompleteAtomicBooleanAlgebra}(\\alpha)$$$

Lean4

/-- Every atomic complete Boolean algebra is completely atomic.

This is not made an instance to avoid typeclass loops. -/
-- See note [reducible non-instances]

abbrev toCompleteAtomicBooleanAlgebra {α} [CompleteBooleanAlgebra α] [IsAtomic α] : CompleteAtomicBooleanAlgebra α
    where
  __ := ‹CompleteBooleanAlgebra α›
  iInf_iSup_eq
    f := BooleanAlgebra.eq_iff_atom_le_iff.2 fun a ha => by simp only [le_iInf_iff, ha.le_iSup, Classical.skolem]

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