Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-05 09:52 4dfbcac3

View on Github →

feat({data/{finset,set},order/filter}/pointwise): More basic API (#13899) More basic lemmas about pointwise operations on set/finset/filter. Also make the three APIs more consistent with each other.

Estimated changes

added theorem finset.div_eq_empty
added theorem finset.div_nonempty
deleted theorem finset.div_nonempty_iff
added theorem finset.div_subset_iff
added theorem finset.div_union
added theorem finset.mul_eq_empty
added theorem finset.mul_nonempty
deleted theorem finset.mul_nonempty_iff
added theorem finset.mul_subset_iff
added theorem finset.mul_union
modified theorem finset.singleton_smul
added theorem finset.smul_eq_empty
modified theorem finset.smul_nonempty_iff
modified theorem finset.smul_singleton
added theorem finset.smul_subset_iff
added theorem finset.smul_union
modified theorem finset.subset_vsub
added theorem finset.union_div
added theorem finset.union_mul
added theorem finset.union_smul
added theorem finset.union_vsub
added theorem finset.vsub_eq_empty
added theorem finset.vsub_nonempty
deleted theorem finset.vsub_nonempty_iff
added theorem finset.vsub_subset_iff
added theorem finset.vsub_union
modified theorem set.Union_div
modified theorem set.Union_div_left_image
modified theorem set.Union_div_right_image
modified theorem set.Union_mul
modified theorem set.Union_mul_left_image
modified theorem set.Union_mul_right_image
modified theorem set.Union_smul
modified theorem set.Union_smul_left_image
modified theorem set.Union_smul_right_image
modified theorem set.div_Union
added theorem set.div_eq_empty
modified theorem set.div_inter_subset
modified theorem set.div_mem_div
added theorem set.div_nonempty
modified theorem set.div_subset_div
modified theorem set.div_subset_div_left
modified theorem set.div_subset_div_right
added theorem set.div_subset_iff
modified theorem set.image_one
modified theorem set.inter_div_subset
modified theorem set.inter_mul_subset
modified theorem set.inter_smul_subset
modified theorem set.mem_one
deleted theorem set.mem_smul_of_mem
modified theorem set.mul_Union
added theorem set.mul_eq_empty
modified theorem set.mul_inter_subset
modified theorem set.mul_mem_mul
added theorem set.mul_nonempty
added theorem set.mul_subset_iff
modified theorem set.mul_subset_mul
modified theorem set.mul_subset_mul_left
modified theorem set.mul_subset_mul_right
added theorem set.nonempty.div
modified theorem set.one_mem_one
modified theorem set.one_nonempty
modified theorem set.one_subset
modified theorem set.singleton_div_singleton
modified theorem set.singleton_mul_singleton
modified theorem set.singleton_one
modified theorem set.smul_Union
added theorem set.smul_eq_empty
modified theorem set.smul_inter_subset
modified theorem set.smul_mem_smul
modified theorem set.smul_mem_smul_set
added theorem set.smul_nonempty
added theorem set.smul_set_eq_empty
added theorem set.smul_set_nonempty
modified theorem set.smul_subset_smul
modified theorem set.smul_subset_smul_left
modified theorem set.smul_subset_smul_right
added theorem set.subset_one_iff_eq
added theorem set.vsub_eq_empty
added theorem set.vsub_nonempty
modified theorem set.vsub_subset_iff
modified theorem set.vsub_subset_vsub
modified theorem set.vsub_subset_vsub_left
modified theorem set.vsub_subset_vsub_right
added theorem filter.div_pure
added theorem filter.inv_eq_bot_iff
added theorem filter.inv_pure
added theorem filter.mul_pure
added theorem filter.pure_div
added theorem filter.pure_div_pure
added theorem filter.pure_mul
added theorem filter.pure_mul_pure
added theorem filter.pure_smul
added theorem filter.pure_smul_pure
added theorem filter.pure_vsub
added theorem filter.pure_vsub_pure
added theorem filter.smul_pure
added theorem filter.vsub_pure