Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-03 20:42 48dea2fd

View on Github →

feat(algebra/pointwise): make instances global (#3240) add image2 and image3, the images of binary and ternary functions cleanup in algebra/pointwise make many variables implicit make many names shorter add some lemmas add more simp lemmas add type set_semiring as alias for set, with semiring instance using union as "addition"

Estimated changes

modified theorem mem_inv_smul_set_iff
deleted def set.add_comm_monoid
deleted def set.comm_monoid
added theorem set.compl_inv
added theorem set.empty_mul
deleted theorem set.empty_pointwise_mul
added theorem set.finite.mul
added def set.fintype_mul
added theorem set.image2_mul
added theorem set.image2_smul
added def set.image_hom
added theorem set.image_inv
added theorem set.image_mul
added theorem set.image_mul_left'
added theorem set.image_mul_left
added theorem set.image_mul_prod
added theorem set.image_mul_right'
added theorem set.image_mul_right
added theorem set.image_one
deleted theorem set.image_pointwise_mul
added theorem set.image_smul
added theorem set.image_smul_prod
added theorem set.inter_inv
added theorem set.inv_mem_inv
added theorem set.inv_preimage
added theorem set.mem_inv
added theorem set.mem_mul
added theorem set.mem_one
deleted theorem set.mem_pointwise_mul
deleted theorem set.mem_pointwise_one
added theorem set.mem_smul
modified theorem set.mem_smul_set
added theorem set.mul_empty
added theorem set.mul_mem_mul
deleted theorem set.mul_mem_pointwise_mul
added theorem set.mul_singleton
added theorem set.mul_subset_mul
added theorem set.mul_union
added theorem set.nonempty.mul
added theorem set.one_mem_one
added theorem set.one_nonempty
added theorem set.one_subset
deleted def set.pointwise_inv
deleted def set.pointwise_mul
deleted theorem set.pointwise_mul_empty
deleted theorem set.pointwise_mul_finite
deleted theorem set.pointwise_mul_union
deleted def set.pointwise_one
deleted def set.pointwise_smul
added def set.set_semiring
added theorem set.singleton_mul
added theorem set.singleton_one
added theorem set.singleton_smul
modified theorem set.smul_mem_smul_set
deleted def set.smul_set
deleted def set.smul_set_action
modified theorem set.smul_set_empty
deleted theorem set.smul_set_eq_image
modified theorem set.smul_set_mono
modified theorem set.smul_set_union
added theorem set.union_inv
added theorem set.union_mul
deleted theorem set.union_pointwise_mul
added theorem set.univ_mul_univ
modified theorem zero_smul_set
added def set.image2
added theorem set.image2_congr'
added theorem set.image2_congr
added theorem set.image2_empty_left
added theorem set.image2_empty_right
added theorem set.image2_image2_left
added theorem set.image2_image_left
added theorem set.image2_image_right
added theorem set.image2_left
added theorem set.image2_right
added theorem set.image2_singleton
added theorem set.image2_subset
added theorem set.image2_swap
added theorem set.image2_union_left
added theorem set.image2_union_right
added def set.image3
added theorem set.image3_congr'
added theorem set.image3_congr
added theorem set.image_eta
added theorem set.image_image2
added theorem set.image_prod
added theorem set.mem_image2
added theorem set.mem_image2_eq
added theorem set.mem_image2_iff
added theorem set.mem_image2_of_mem
added theorem set.mem_image3
added theorem set.nonempty.image2
added theorem set.nonempty_def
added theorem set.finite.image2
modified theorem set.image_add_const_Ici
modified theorem set.image_add_const_Iic
modified theorem set.image_add_const_Iio
modified theorem set.image_add_const_Ioi
modified theorem set.image_neg_Icc
modified theorem set.image_neg_Ici
modified theorem set.image_neg_Ico
modified theorem set.image_neg_Iic
modified theorem set.image_neg_Iio
modified theorem set.image_neg_Ioc
modified theorem set.image_neg_Ioi
modified theorem set.image_neg_Ioo
modified theorem set.preimage_neg_Icc
modified theorem set.preimage_neg_Ici
modified theorem set.preimage_neg_Ico
modified theorem set.preimage_neg_Iic
modified theorem set.preimage_neg_Iio
modified theorem set.preimage_neg_Ioc
modified theorem set.preimage_neg_Ioi
modified theorem set.preimage_neg_Ioo
added theorem set.Union_image_left
added theorem set.Union_image_right
added theorem eq_inv_smul_iff
added theorem inv_smul_eq_iff
deleted theorem filter.map_pointwise_mul
deleted theorem filter.map_pointwise_one
added theorem filter.mem_mul
added theorem filter.mem_one
deleted theorem filter.mem_pointwise_mul
deleted theorem filter.mem_pointwise_one
added theorem filter.mul_mem_mul
added theorem filter.mul_ne_bot
deleted theorem filter.pointwise_mul_one
deleted theorem filter.pointwise_one_mul
modified theorem submodule.mul_subset_mul
modified theorem submodule.pow_subset_pow
modified theorem submodule.smul_def
modified theorem submodule.smul_le_smul
modified theorem ideal.span_singleton_one
added theorem is_open_mul_left
added theorem is_open_mul_right
modified theorem nhds_is_mul_hom
added theorem nhds_mul
deleted theorem nhds_pointwise_mul