Theorem CompleteAtomicBooleanAlgebra.exists_mem_le_of_le_sSup_of_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.exists_mem_le_of_le_sSup_of_isAtomView on Github →