Commit 2023-01-10 21:07 0301e4e3

View on Github →

feat: port Data.Set.Pointwise.Basic (#1188)

depends on: https://github.com/leanprover/std4/pull/83
depends on: https://github.com/JLimperg/aesop/pull/38
depends on: #1447

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Pointwise/Basic.lean

added theorem Group.card_pow_eq_card_pow_card_univ_aux

added theorem Set.Nonempty.div

added theorem Set.Nonempty.div_zero

added theorem Set.Nonempty.inv

added theorem Set.Nonempty.mul

added theorem Set.Nonempty.mul_zero

added theorem Set.Nonempty.of_div_left

added theorem Set.Nonempty.of_div_right

added theorem Set.Nonempty.of_mul_left

added theorem Set.Nonempty.of_mul_right

added theorem Set.Nonempty.one_mem_div

added theorem Set.Nonempty.subset_one_iff

added theorem Set.Nonempty.zero_div

added theorem Set.Nonempty.zero_mul

added theorem Set.add_mul_subset

added theorem Set.bddAbove_mul

added theorem Set.coe_singletonMonoidHom

added theorem Set.coe_singletonMulHom

added theorem Set.coe_singletonOneHom

added theorem Set.compl_inv

added theorem Set.div_empty

added theorem Set.div_eq_empty

added theorem Set.div_inter_subset

added theorem Set.div_interᵢ_subset

added theorem Set.div_interᵢ₂_subset

added theorem Set.div_mem_div

added theorem Set.div_nonempty

added theorem Set.div_singleton

added theorem Set.div_subset_div

added theorem Set.div_subset_div_left

added theorem Set.div_subset_div_right

added theorem Set.div_subset_iff

added theorem Set.div_union

added theorem Set.div_unionᵢ

added theorem Set.div_unionᵢ₂

added theorem Set.div_zero_subset

added theorem Set.empty_div

added theorem Set.empty_mul

added theorem Set.empty_pow

added theorem Set.image2_div

added theorem Set.image2_mul

added theorem Set.image_div

added theorem Set.image_div_prod

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

added theorem Set.image_op_inv

added theorem Set.image_op_mul

added theorem Set.inter_div_subset

added theorem Set.inter_inv

added theorem Set.inter_mul_subset

added theorem Set.interᵢ_div_subset

added theorem Set.interᵢ_inv

added theorem Set.interᵢ_mul_subset

added theorem Set.interᵢ₂_div_subset

added theorem Set.interᵢ₂_mul_subset

added theorem Set.inv_empty

added theorem Set.inv_insert

added theorem Set.inv_mem_inv

added theorem Set.inv_preimage

added theorem Set.inv_range

added theorem Set.inv_singleton

added theorem Set.inv_subset

added theorem Set.inv_subset_inv

added theorem Set.inv_univ

added theorem Set.isUnit_iff

added theorem Set.isUnit_iff_singleton

added theorem Set.isUnit_singleton

added theorem Set.mem_div

added theorem Set.mem_inv

added theorem Set.mem_mul

added theorem Set.mem_one

added theorem Set.mul_add_subset

added theorem Set.mul_empty

added theorem Set.mul_eq_empty

added theorem Set.mul_inter_subset

added theorem Set.mul_interᵢ_subset

added theorem Set.mul_interᵢ₂_subset

added theorem Set.mul_mem_mul

added theorem Set.mul_nonempty

added theorem Set.mul_singleton

added theorem Set.mul_subset_iff

added theorem Set.mul_subset_mul

added theorem Set.mul_subset_mul_left

added theorem Set.mul_subset_mul_right

added theorem Set.mul_union

added theorem Set.mul_unionᵢ

added theorem Set.mul_unionᵢ₂

added theorem Set.mul_univ

added theorem Set.mul_univ_of_one_mem

added theorem Set.mul_zero_subset

added theorem Set.nonempty_inv

added theorem Set.not_one_mem_div_iff

added theorem Set.nsmul_univ

added theorem Set.one_mem_div_iff

added theorem Set.one_mem_one

added theorem Set.one_nonempty

added theorem Set.one_subset

added theorem Set.pow_mem_pow

added theorem Set.pow_subset_pow

added theorem Set.pow_subset_pow_of_one_mem

added theorem Set.preimage_div_preimage_subset

added theorem Set.preimage_mul_left_one'

added theorem Set.preimage_mul_left_one

added theorem Set.preimage_mul_left_singleton

added theorem Set.preimage_mul_preimage_subset

added theorem Set.preimage_mul_right_one'

added theorem Set.preimage_mul_right_one

added theorem Set.preimage_mul_right_singleton

added theorem Set.singletonMonoidHom_apply

added theorem Set.singletonMulHom_apply

added theorem Set.singleton_div

added theorem Set.singleton_div_singleton

added theorem Set.singleton_mul

added theorem Set.singleton_mul_singleton

added theorem Set.singleton_one

added theorem Set.subset_mul_left

added theorem Set.subset_mul_right

added theorem Set.subset_one_iff_eq

added theorem Set.union_div

added theorem Set.union_inv

added theorem Set.union_mul

added theorem Set.unionᵢ_div

added theorem Set.unionᵢ_div_left_image

added theorem Set.unionᵢ_div_right_image

added theorem Set.unionᵢ_inv

added theorem Set.unionᵢ_mul

added theorem Set.unionᵢ_mul_left_image

added theorem Set.unionᵢ_mul_right_image

added theorem Set.unionᵢ₂_div

added theorem Set.unionᵢ₂_mul

added theorem Set.univ_mul

added theorem Set.univ_mul_of_one_mem

added theorem Set.univ_mul_univ

added theorem Set.univ_pow

added theorem Set.zero_div_subset

added theorem Set.zero_mul_subset