Commit 2026-02-04 14:37 2fe8173d

View on Github →

feat(Order): distributivity of himp sdiff over iSup iInf (#34781)

Estimated changes

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

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

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

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

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