Commit 2025-02-14 12:41 71f056b2

View on Github →

feat: a ≤ b \ c ↔ ∀ d, b ≤ c ⊔ d → a ≤ d (#21601) Rename le_sdiff_iff to le_sdiff_right (which further matches sdiff_eq_right) to free the name. Moves:

le_sdiff_iff -> le_sdiff_right
himp_le_iff -> himp_le_left

Estimated changes

Modified Mathlib/Combinatorics/SetFamily/Compression/UV.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean

Modified Mathlib/Order/BooleanAlgebra.lean

deleted theorem himp_le_iff

added theorem himp_le_left

deleted theorem le_sdiff_iff

added theorem le_sdiff_right

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

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

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

Modified Mathlib/Order/SymmDiff.lean