Commit 2024-09-10 12:58 9d81c969

View on Github →

chore(Algebra/Group/Pointwise/Set): Incorporate lemmas from Data.Set.Pointwise.SMul (#16487) All these lemmas can be moved earlier at no cost.

Estimated changes

added theorem Set.Nonempty.smul
added theorem Set.Nonempty.smul_set
added theorem Set.Nonempty.vsub
added theorem Set.empty_smul
added theorem Set.empty_vsub
added theorem Set.iInter_smul_subset
added theorem Set.iInter_vsub_subset
added theorem Set.iUnion_smul
added theorem Set.iUnion_smul_set
added theorem Set.iUnion_vsub
added theorem Set.iUnion₂_smul
added theorem Set.iUnion₂_vsub
added theorem Set.image2_smul
added theorem Set.image2_vsub
added theorem Set.image_smul
added theorem Set.image_smul_comm
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.mem_smul
added theorem Set.mem_smul_set
added theorem Set.mem_vsub
added theorem Set.range_smul
added theorem Set.range_smul_range
added theorem Set.singleton_smul
added theorem Set.singleton_vsub
added theorem Set.smul_empty
added theorem Set.smul_eq_empty
added theorem Set.smul_iInter_subset
added theorem Set.smul_iUnion
added theorem Set.smul_iUnion₂
added theorem Set.smul_inter_subset
added theorem Set.smul_mem_smul
added theorem Set.smul_mem_smul_set
added theorem Set.smul_nonempty
added theorem Set.smul_set_empty
added theorem Set.smul_set_eq_empty
added theorem Set.smul_set_iUnion
added theorem Set.smul_set_iUnion₂
added theorem Set.smul_set_mono
added theorem Set.smul_set_nonempty
added theorem Set.smul_set_range
added theorem Set.smul_set_singleton
added theorem Set.smul_set_union
added theorem Set.smul_singleton
added theorem Set.smul_subset_iff
added theorem Set.smul_subset_smul
added theorem Set.smul_union
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_iInter_subset
added theorem Set.vsub_iUnion
added theorem Set.vsub_iUnion₂
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_union
deleted theorem Set.Nonempty.of_smul_left
deleted theorem Set.Nonempty.of_vsub_left
deleted theorem Set.Nonempty.smul
deleted theorem Set.Nonempty.smul_set
deleted theorem Set.Nonempty.vsub
deleted theorem Set.empty_smul
deleted theorem Set.empty_vsub
deleted theorem Set.iInter_smul_subset
deleted theorem Set.iInter_vsub_subset
deleted theorem Set.iInter₂_smul_subset
deleted theorem Set.iInter₂_vsub_subset
deleted theorem Set.iUnion_smul
deleted theorem Set.iUnion_smul_set
deleted theorem Set.iUnion_vsub
deleted theorem Set.iUnion₂_smul
deleted theorem Set.iUnion₂_vsub
deleted theorem Set.image2_smul
deleted theorem Set.image2_vsub
deleted theorem Set.image_smul
deleted theorem Set.image_smul_comm
deleted theorem Set.image_smul_prod
deleted theorem Set.image_vsub_prod
deleted theorem Set.inter_smul_subset
deleted theorem Set.inter_vsub_subset
deleted theorem Set.mem_smul
deleted theorem Set.mem_smul_set
deleted theorem Set.mem_vsub
deleted theorem Set.range_smul
deleted theorem Set.range_smul_range
deleted theorem Set.singleton_smul
deleted theorem Set.singleton_vsub
deleted theorem Set.smul_empty
deleted theorem Set.smul_eq_empty
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_inter_subset
deleted theorem Set.smul_mem_smul
deleted theorem Set.smul_mem_smul_set
deleted theorem Set.smul_nonempty
deleted theorem Set.smul_set_empty
deleted theorem Set.smul_set_eq_empty
deleted theorem Set.smul_set_iUnion
deleted theorem Set.smul_set_iUnion₂
deleted theorem Set.smul_set_inter_subset
deleted theorem Set.smul_set_mono
deleted theorem Set.smul_set_nonempty
deleted theorem Set.smul_set_range
deleted theorem Set.smul_set_singleton
deleted theorem Set.smul_set_subset_iff
deleted theorem Set.smul_set_subset_smul
deleted theorem Set.smul_set_union
deleted theorem Set.smul_singleton
deleted theorem Set.smul_subset_iff
deleted theorem Set.smul_subset_smul
deleted theorem Set.smul_subset_smul_left
deleted theorem Set.smul_union
deleted theorem Set.union_smul
deleted theorem Set.union_vsub
deleted theorem Set.vsub_empty
deleted theorem Set.vsub_eq_empty
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_inter_subset
deleted theorem Set.vsub_mem_vsub
deleted theorem Set.vsub_nonempty
deleted theorem Set.vsub_self_mono
deleted theorem Set.vsub_singleton
deleted theorem Set.vsub_subset_iff
deleted theorem Set.vsub_subset_vsub
deleted theorem Set.vsub_subset_vsub_left
deleted theorem Set.vsub_union