Commit 2024-09-30 20:40 d5d186a1

View on Github →

feat(Algebra/Group/Pointwise/Set/Basic): sInter and sUnion forms of pointwise operations (#17253) Provides sInter and sUnion versions of pointwise algebraic operations on sets. Needed in #17029

Estimated changes

added theorem Set.div_sInter_subset
added theorem Set.div_sUnion
added theorem Set.mul_sInter_subset
added theorem Set.mul_sUnion
added theorem Set.sInter_div_subset
added theorem Set.sInter_inv
added theorem Set.sInter_mul_subset
added theorem Set.sInter_smul_subset
added theorem Set.sInter_vsub_subset
added theorem Set.sUnion_div
added theorem Set.sUnion_inv
added theorem Set.sUnion_mul
added theorem Set.sUnion_smul
added theorem Set.sUnion_vsub
added theorem Set.smul_sInter_subset
added theorem Set.smul_sUnion
added theorem Set.smul_set_sUnion
added theorem Set.vsub_sInter_subset
added theorem Set.vsub_sUnion
added theorem Set.image2_sUnion_left