Commit 2025-11-21 03:35 0d202438

View on Github →

feat: add CompleteAtomicBooleanAlgebra is order isomorphic to set of its atoms (#31724) CompleteAtomicBooleanAlgebra is order isomorphic to the set of its atoms. This PR add a OrderIso definition that prove this fact.

Estimated changes

Modified Mathlib/Order/Atoms.lean

added theorem CompleteAtomicBooleanAlgebra.eq_setOf_le_sSup_and_isAtom

added theorem CompleteAtomicBooleanAlgebra.exists_mem_le_of_le_sSup_of_isAtom

added def CompleteAtomicBooleanAlgebra.toSetOfIsAtom