2025-06-15 18:44
Mathlib/Order/CompleteBooleanAlgebra.lean
refactor: prove assumptions of `CompleteBooleanAlgebra` (#25909) …
Added Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.inf_sSup_le_iSup_inf