Theorem CompleteAtomicBooleanAlgebra.eq_setOf_le_sSup_and_isAtom

Modification history

2025-11-21 03:35
Mathlib/Order/Atoms.lean
feat: add CompleteAtomicBooleanAlgebra is order isomorphic to set of its atoms (#31724) …
Added CompleteAtomicBooleanAlgebra.eq_setOf_le_sSup_and_isAtomView on Github →