Commit 2025-06-15 18:44 6abd1889

View on Github →

refactor: prove assumptions of CompleteBooleanAlgebra (#25909)

Add proofs for inf_sSup_le_iSup_inf and iInf_sup_le_sup_sInf
Remove proofs of those for instances of CompleteBooleanAlgebra

Estimated changes

Modified Mathlib/Data/Fintype/Order.lean

Modified Mathlib/Order/Atoms.lean

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.iInf_sup_le_sup_sInf

added theorem Order.Frame.MinimalAxioms.Order.Coframe.MinimalAxioms.CompleteDistribLattice.MinimalAxioms.CompletelyDistribLattice.MinimalAxioms.inf_sSup_le_iSup_inf