Commit 2025-03-20 16:39 3a843e76

View on Github →

chore(Algebra/Group): split iUnion/iInter from long file Pointwise/Set/Basic.lean (#23152) This PR splits up the long file Algebra.Group.Pointwise.Set.Basic by taking out all results involving the complete lattice structure on Set: these now live in Pointwise.Set.Lattice. We get a surprising reduction in downstream imports, since apparently we don't care much about order theory in that area of the library!

Estimated changes

deleted theorem Set.div_iInter_subset
deleted theorem Set.div_iInter₂_subset
deleted theorem Set.div_iUnion
deleted theorem Set.div_iUnion₂
deleted theorem Set.div_sInter_subset
deleted theorem Set.div_sUnion
deleted theorem Set.iInter_div_subset
deleted theorem Set.iInter_inv
deleted theorem Set.iInter_mul_subset
deleted theorem Set.iInter_smul_subset
deleted theorem Set.iInter_vsub_subset
deleted theorem Set.iInter₂_div_subset
deleted theorem Set.iInter₂_mul_subset
deleted theorem Set.iInter₂_smul_subset
deleted theorem Set.iInter₂_vsub_subset
deleted theorem Set.iUnion_div
deleted theorem Set.iUnion_div_left_image
deleted theorem Set.iUnion_inv
deleted theorem Set.iUnion_mul
deleted theorem Set.iUnion_mul_left_image
deleted theorem Set.iUnion_smul
deleted theorem Set.iUnion_smul_set
deleted theorem Set.iUnion_vsub
deleted theorem Set.iUnion₂_div
deleted theorem Set.iUnion₂_mul
deleted theorem Set.iUnion₂_smul
deleted theorem Set.iUnion₂_vsub
deleted theorem Set.mul_iInter_subset
deleted theorem Set.mul_iInter₂_subset
deleted theorem Set.mul_iUnion
deleted theorem Set.mul_iUnion₂
deleted theorem Set.mul_sInter_subset
deleted theorem Set.mul_sUnion
deleted theorem Set.sInter_div_subset
deleted theorem Set.sInter_inv
deleted theorem Set.sInter_mul_subset
deleted theorem Set.sInter_smul_subset
deleted theorem Set.sInter_vsub_subset
deleted theorem Set.sUnion_div
deleted theorem Set.sUnion_inv
deleted theorem Set.sUnion_mul
deleted theorem Set.sUnion_smul
deleted theorem Set.sUnion_vsub
deleted theorem Set.smul_iInter_subset
deleted theorem Set.smul_iInter₂_subset
deleted theorem Set.smul_iUnion
deleted theorem Set.smul_iUnion₂
deleted theorem Set.smul_sInter_subset
deleted theorem Set.smul_sUnion
deleted theorem Set.smul_set_iUnion
deleted theorem Set.smul_set_iUnion₂
deleted theorem Set.smul_set_sUnion
deleted theorem Set.vsub_iInter_subset
deleted theorem Set.vsub_iInter₂_subset
deleted theorem Set.vsub_iUnion
deleted theorem Set.vsub_iUnion₂
deleted theorem Set.vsub_sInter_subset
deleted theorem Set.vsub_sUnion
added theorem Set.div_iInter_subset
added theorem Set.div_iUnion
added theorem Set.div_iUnion₂
added theorem Set.div_sInter_subset
added theorem Set.div_sUnion
added theorem Set.iInter_div_subset
added theorem Set.iInter_inv
added theorem Set.iInter_mul_subset
added theorem Set.iInter_smul_subset
added theorem Set.iInter_vsub_subset
added theorem Set.iUnion_div
added theorem Set.iUnion_inv
added theorem Set.iUnion_mul
added theorem Set.iUnion_smul
added theorem Set.iUnion_smul_set
added theorem Set.iUnion_vsub
added theorem Set.iUnion₂_div
added theorem Set.iUnion₂_mul
added theorem Set.iUnion₂_smul
added theorem Set.iUnion₂_vsub
added theorem Set.mul_iInter_subset
added theorem Set.mul_iUnion
added theorem Set.mul_iUnion₂
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_iInter_subset
added theorem Set.smul_iUnion
added theorem Set.smul_iUnion₂
added theorem Set.smul_sInter_subset
added theorem Set.smul_sUnion
added theorem Set.smul_set_iUnion
added theorem Set.smul_set_iUnion₂
added theorem Set.smul_set_sUnion
added theorem Set.vsub_iInter_subset
added theorem Set.vsub_iUnion
added theorem Set.vsub_iUnion₂
added theorem Set.vsub_sInter_subset
added theorem Set.vsub_sUnion