Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-17 22:40 cf8c5ff1

View on Github →

feat(algebra/pointwise): Subtraction/division of sets (#12694) Define pointwise subtraction/division on set.

Estimated changes

added theorem set.Inter_div_subset
added theorem set.Union_div
added theorem set.Union₂_div
added theorem set.div_Inter_subset
added theorem set.div_Union
added theorem set.div_Union₂
added theorem set.div_empty
added theorem set.div_inter_subset
added theorem set.div_mem_div
added theorem set.div_singleton
added theorem set.div_subset_div
added theorem set.div_union
added theorem set.empty_div
added theorem set.image2_div
added theorem set.image_div_prod
added theorem set.inter_div_subset
added theorem set.mem_div
added theorem set.singleton_div
added theorem set.union_div