Commit 2024-10-17 19:56 a4d283b5

View on Github →

feat(Order/BooleanAlgebra, Data/Set/Basic): diff_le_diff_iff (#17876) This PR adds a lemma stating that, for x, y ≤ z in a boolean algebra, we have z \ x ≤ z \ y iff y ≤ x. We also add the same lemma for sets/finsets.

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.sdiff_subset_sdiff_iff_subset

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.diff_subset_diff_iff_subset

Modified Mathlib/Order/BooleanAlgebra.lean

added theorem sdiff_le_sdiff_iff_le