Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 21:01 9e799a08

View on Github →

feat(algebra/pointwise): Scalar multiplication lemmas (#11486) This proves a bunch of lemmas about pointwise scalar multiplication of sets, moves has_vsub to algebra.group.defs and pointwise vsub lemmas to algebra.pointwise. I'm also adding a few sections because having {s t : set α} is nice for multiplication but not for scalar multiplication.

Estimated changes

Modified src/algebra/add_torsor.lean

deleted theorem set.empty_vsub

deleted theorem set.finite.vadd

deleted theorem set.finite.vsub

deleted theorem set.mem_vsub

deleted theorem set.set_vadd_singleton

deleted theorem set.singleton_vsub

deleted theorem set.vadd_subset_vadd

deleted theorem set.vsub_empty

deleted theorem set.vsub_mem_vsub

deleted theorem set.vsub_self_mono

deleted theorem set.vsub_singleton

deleted theorem set.vsub_subset_iff

deleted theorem set.vsub_subset_vsub

Modified src/algebra/group/defs.lean

Modified src/algebra/pointwise.lean

modified theorem mem_inv_smul_set_iff₀

modified theorem mem_smul_set_iff_inv_smul_mem₀

modified theorem preimage_smul_inv₀

modified theorem preimage_smul₀

added theorem set.Inter_mul_subset

added theorem set.Inter_smul_subset

added theorem set.Inter_vsub_subset

added theorem set.Inter₂_mul_subset

added theorem set.Inter₂_smul_subset

added theorem set.Inter₂_vsub_subset

modified theorem set.Union_mul

modified theorem set.Union_mul_left_image

modified theorem set.Union_mul_right_image

added theorem set.Union_smul

added theorem set.Union_smul_left_image

added theorem set.Union_smul_right_image

added theorem set.Union_vsub

added theorem set.Union_vsub_left_image

added theorem set.Union_vsub_right_image

added theorem set.Union₂_mul

added theorem set.Union₂_smul

added theorem set.Union₂_vsub

modified theorem set.empty_mul

added theorem set.empty_smul

added theorem set.empty_vsub

added theorem set.finite.smul_set

added theorem set.finite.vsub

modified theorem set.image2_mul

modified theorem set.image2_smul

added theorem set.image2_vsub

modified theorem set.image_mul_left

modified theorem set.image_mul_prod

modified theorem set.image_mul_right'

modified theorem set.image_mul_right

modified theorem set.image_one

modified theorem set.image_smul

modified theorem set.image_smul_prod

added theorem set.image_vsub_prod

added theorem set.inter_mul_subset

added theorem set.inter_smul_subset

added theorem set.inter_vsub_subset

modified theorem set.mem_mul

modified theorem set.mem_one

modified theorem set.mem_smul

modified theorem set.mem_smul_of_mem

modified theorem set.mem_smul_set

added theorem set.mem_vsub

added theorem set.mul_Inter_subset

added theorem set.mul_Inter₂_subset

modified theorem set.mul_Union

added theorem set.mul_Union₂

modified theorem set.mul_empty

added theorem set.mul_inter_subset

modified theorem set.mul_mem_mul

modified theorem set.mul_singleton

modified theorem set.mul_subset_mul

modified theorem set.mul_subset_mul_left

modified theorem set.mul_subset_mul_right

modified theorem set.mul_union

added theorem set.mul_univ

added theorem set.neg_smul_set

modified theorem set.one_mem_one

modified theorem set.one_nonempty

modified theorem set.one_subset

modified theorem set.preimage_mul_left_one

modified theorem set.preimage_mul_right_one'

modified theorem set.preimage_mul_right_one

modified theorem set.range_smul_range

modified theorem set.singleton_mul

modified def set.singleton_mul_hom

modified theorem set.singleton_mul_singleton

modified theorem set.singleton_one

modified theorem set.singleton_smul

added theorem set.singleton_smul_singleton

added theorem set.singleton_vsub

added theorem set.singleton_vsub_singleton

added theorem set.smul_Inter_subset

added theorem set.smul_Inter₂_subset

added theorem set.smul_Union

added theorem set.smul_Union₂

added theorem set.smul_empty

added theorem set.smul_inter_subset

added theorem set.smul_mem_smul

modified theorem set.smul_mem_smul_set

added theorem set.smul_set_Inter_subset

added theorem set.smul_set_Inter₂_subset

added theorem set.smul_set_Union

added theorem set.smul_set_Union₂

modified theorem set.smul_set_empty

modified theorem set.smul_set_inter_subset

modified theorem set.smul_set_mono

added theorem set.smul_set_neg

added theorem set.smul_set_singleton

modified theorem set.smul_set_union

added theorem set.smul_set_univ

modified theorem set.smul_singleton

added theorem set.smul_subset_iff

added theorem set.smul_subset_smul

added theorem set.smul_subset_smul_left

added theorem set.smul_subset_smul_right

added theorem set.smul_union

added theorem set.smul_univ

added theorem set.subset_mul_left

added theorem set.subset_mul_right

modified theorem set.union_mul

added theorem set.union_smul

added theorem set.union_vsub

added theorem set.univ_mul

added theorem set.vsub_Inter_subset

added theorem set.vsub_Inter₂_subset

added theorem set.vsub_Union

added theorem set.vsub_Union₂

added theorem set.vsub_empty

added theorem set.vsub_inter_subset

added theorem set.vsub_mem_vsub

added theorem set.vsub_self_mono

added theorem set.vsub_singleton

added theorem set.vsub_subset_iff

added theorem set.vsub_subset_vsub

added theorem set.vsub_subset_vsub_left

added theorem set.vsub_subset_vsub_right

added theorem set.vsub_union

modified theorem set_smul_subset_iff₀

modified theorem set_smul_subset_set_smul_iff₀

modified theorem smul_mem_smul_set_iff₀

added theorem smul_set_univ₀

added theorem smul_univ₀

modified theorem subset_set_smul_iff₀

modified theorem subsingleton_zero_smul_set

added theorem zero_mem_smul_iff

added theorem zero_mem_smul_set

added theorem zero_mem_smul_set_iff

modified theorem zero_smul_set

modified theorem zero_smul_subset

Modified src/analysis/convex/star.lean