Commit 2023-01-13 09:15 6d86a6ac

View on Github →

feat: port Data.Set.Pointwise.SMul (#1473)

Estimated changes

Modified Mathlib.lean

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

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

added theorem Set.Nonempty.of_smul_left

added theorem Set.Nonempty.of_smul_right

added theorem Set.Nonempty.of_vsub_left

added theorem Set.Nonempty.of_vsub_right

added theorem Set.Nonempty.smul

added theorem Set.Nonempty.smul_set

added theorem Set.Nonempty.smul_zero

added theorem Set.Nonempty.vsub

added theorem Set.Nonempty.zero_smul

added theorem Set.empty_smul

added theorem Set.empty_vsub

added theorem Set.image2_smul

added theorem Set.image2_vsub

added theorem Set.image_smul

added theorem Set.image_smul_prod

added theorem Set.image_vsub_prod

added theorem Set.inter_smul_subset

added theorem Set.inter_vsub_subset

added theorem Set.interᵢ_smul_subset

added theorem Set.interᵢ_vsub_subset

added theorem Set.interᵢ₂_smul_subset

added theorem Set.interᵢ₂_vsub_subset

added theorem Set.mem_inv_smul_set_iff

added theorem Set.mem_inv_smul_set_iff₀

added theorem Set.mem_smul

added theorem Set.mem_smul_set

added theorem Set.mem_smul_set_iff_inv_smul_mem

added theorem Set.mem_smul_set_iff_inv_smul_mem₀

added theorem Set.mem_vsub

added theorem Set.neg_smul_set

added theorem Set.op_smul_inter_ne_empty_iff

added theorem Set.pairwiseDisjoint_smul_iff

added theorem Set.preimage_smul

added theorem Set.preimage_smul_inv

added theorem Set.preimage_smul_inv₀

added theorem Set.preimage_smul₀

added theorem Set.range_smul_range

added theorem Set.set_smul_subset_iff

added theorem Set.set_smul_subset_iff₀

added theorem Set.set_smul_subset_set_smul_iff

added theorem Set.set_smul_subset_set_smul_iff₀

added 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_empty

added theorem Set.smul_eq_empty

added theorem Set.smul_inter_ne_empty_iff'

added theorem Set.smul_inter_ne_empty_iff

added theorem Set.smul_inter_subset

added theorem Set.smul_interᵢ_subset

added theorem Set.smul_interᵢ₂_subset

added theorem Set.smul_mem_smul

added theorem Set.smul_mem_smul_set

added theorem Set.smul_mem_smul_set_iff

added theorem Set.smul_mem_smul_set_iff₀

added theorem Set.smul_nonempty

added theorem Set.smul_set_Union

added theorem Set.smul_set_empty

added theorem Set.smul_set_eq_empty

added theorem Set.smul_set_inter

added theorem Set.smul_set_inter_subset

added theorem Set.smul_set_interᵢ_subset

added theorem Set.smul_set_interᵢ₂_subset

added theorem Set.smul_set_inter₀

added theorem Set.smul_set_mono

added theorem Set.smul_set_neg

added theorem Set.smul_set_nonempty

added theorem Set.smul_set_range

added theorem Set.smul_set_sdiff

added theorem Set.smul_set_sdiff₀

added theorem Set.smul_set_singleton

added theorem Set.smul_set_subset_iff

added theorem Set.smul_set_symm_diff

added theorem Set.smul_set_symm_diff₀

added theorem Set.smul_set_union

added theorem Set.smul_set_unionᵢ₂

added theorem Set.smul_set_univ

added theorem Set.smul_set_univ₀

added 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_unionᵢ

added theorem Set.smul_unionᵢ₂

added theorem Set.smul_univ

added theorem Set.smul_univ₀'

added theorem Set.smul_univ₀

added theorem Set.smul_zero_subset

added theorem Set.subset_set_smul_iff

added theorem Set.subset_set_smul_iff₀

added theorem Set.subsingleton_zero_smul_set

added theorem Set.union_smul

added theorem Set.union_vsub

added theorem Set.unionᵢ_inv_smul

added theorem Set.unionᵢ_op_smul_set

added theorem Set.unionᵢ_smul

added theorem Set.unionᵢ_smul_eq_setOf_exists

added theorem Set.unionᵢ_smul_left_image

added theorem Set.unionᵢ_smul_right_image

added theorem Set.unionᵢ_smul_set

added theorem Set.unionᵢ_vsub

added theorem Set.unionᵢ_vsub_left_image

added theorem Set.unionᵢ_vsub_right_image

added theorem Set.unionᵢ₂_smul

added theorem Set.unionᵢ₂_vsub

added theorem Set.vsub_empty

added theorem Set.vsub_eq_empty

added theorem Set.vsub_inter_subset

added theorem Set.vsub_interᵢ_subset

added theorem Set.vsub_interᵢ₂_subset

added theorem Set.vsub_mem_vsub

added theorem Set.vsub_nonempty

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

added theorem Set.vsub_unionᵢ

added theorem Set.vsub_unionᵢ₂

added theorem Set.zero_mem_smul_iff

added theorem Set.zero_mem_smul_set

added theorem Set.zero_mem_smul_set_iff

added theorem Set.zero_smul_set

added theorem Set.zero_smul_set_subset

added theorem Set.zero_smul_subset