Commit 2025-03-21 02:30 08b4fc2a

View on Github →

feat(Set): lemmas about set difference (#22253) We add some API lemmas about set difference and strict subsets.

Estimated changes

Modified Mathlib/Data/Matroid/Circuit.lean

Modified Mathlib/Data/Matroid/Closure.lean

Modified Mathlib/Data/Matroid/IndepAxioms.lean

Modified Mathlib/Data/Set/Basic.lean

modified theorem Set.diff_inter_diff

added theorem Set.diff_inter_distrib_right

added theorem Set.diff_inter_right_comm

added theorem Set.diff_union_diff_cancel'

added theorem Set.inter_diff_right_comm

added theorem Set.inter_ssubset_left_iff

added theorem Set.inter_ssubset_right_iff

added theorem Set.ssubset_union_left_iff

added theorem Set.ssubset_union_right_iff

Modified Mathlib/Data/Set/Disjoint.lean

added theorem HasSubset.Subset.diff_ssubset_of_nonempty

added theorem Set.diff_ssubset_left_iff

Modified Mathlib/Data/Set/Insert.lean

added theorem HasSubset.Subset.ssubset_of_mem_not_mem

deleted theorem Set.diff_singleton_sSubset

added theorem Set.diff_singleton_ssubset

added theorem Set.insert_diff_insert

Modified Mathlib/Order/BooleanAlgebra.lean

added theorem sdiff_lt_left

Modified Mathlib/Order/Heyting/Basic.lean

added theorem sdiff_sup_sdiff_cancel'