Commit 2023-04-02 16:12 0ec696f2

View on Github →

feat: a • t ⊆ s • t (#3227) Match https://github.com/leanprover-community/mathlib/pull/18697

Estimated changes

Modified Mathlib/Data/Finset/NAry.lean

modified theorem Finset.image_subset_image₂_right

added theorem Finset.image₂_insert_left

added theorem Finset.image₂_insert_right

added theorem Finset.image₂_inter_union_subset_union

added theorem Finset.image₂_subset_iff_left

added theorem Finset.image₂_subset_iff_right

added theorem Finset.image₂_union_inter_subset_union

Modified Mathlib/Data/Finset/Pointwise.lean

added theorem Finset.bunionᵢ_op_smul_finset

added theorem Finset.inter_div_union_subset_union

added theorem Finset.inter_mul_union_subset_union

added theorem Finset.inter_smul_union_subset_union

added theorem Finset.mul_subset_iff_left

added theorem Finset.mul_subset_iff_right

added theorem Finset.op_smul_finset_mul_eq_mul_smul_finset

added theorem Finset.op_smul_finset_smul_eq_smul_smul_finset

added theorem Finset.op_smul_finset_subset_mul

deleted theorem Finset.smul_finset_mem_smul_finset

added theorem Finset.smul_finset_subset_smul

added theorem Finset.smul_mem_smul_finset

added theorem Finset.union_div_inter_subset_union

added theorem Finset.union_mul_inter_subset_union

added theorem Finset.union_smul_inter_subset_union

Modified Mathlib/Data/Set/NAry.lean

added theorem Set.image2_insert_left

added theorem Set.image2_insert_right

added theorem Set.image2_inter_union_subset_union

added theorem Set.image2_subset_iff_left

added theorem Set.image2_subset_iff_right

modified theorem Set.image2_swap

added theorem Set.image2_union_inter_subset_union

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

added theorem Set.inter_div_union_subset_union

added theorem Set.inter_mul_union_subset_union

added theorem Set.union_div_inter_subset_union

added theorem Set.union_mul_inter_subset_union

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

added theorem Set.inter_smul_union_subset_union

added theorem Set.inter_vsub_union_subset_union

added theorem Set.mul_subset_iff_left

added theorem Set.mul_subset_iff_right

added theorem Set.op_smul_set_mul_eq_mul_smul_set

added theorem Set.op_smul_set_smul_eq_smul_smul_set

added theorem Set.op_smul_set_subset_mul

added theorem Set.smul_set_subset_smul

added theorem Set.union_smul_inter_subset_union

added theorem Set.union_vsub_inter_subset_union

modified theorem Set.unionᵢ_op_smul_set