Commit 2024-12-18 16:02 78c7971c

View on Github →

feat(Data/Set/Lattice): image2 lemmas (#20020) Also add spaces after ⋃₀ for uniformity with ⋂₀. From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

modified theorem Set.Nonempty.of_sUnion

modified theorem Set.Nonempty.of_sUnion_eq_univ

added theorem Set.biInter_image2

added theorem Set.biUnion_image2

modified theorem Set.compl_sInter

modified theorem Set.compl_sUnion

added theorem Set.iInter_union_iInter

added theorem Set.iInter₂_union_iInter₂

added theorem Set.iUnion_inter_iUnion

added theorem Set.iUnion₂_inter_iUnion₂

modified theorem Set.nonempty_sUnion

modified theorem Set.not_mem_of_not_mem_sUnion

modified theorem Set.preimage_sUnion

modified theorem Set.prod_sUnion

modified theorem Set.sInter_eq_compl_sUnion_compl

added theorem Set.sInter_image2

modified theorem Set.sInter_image

modified theorem Set.sUnion_diff_singleton_empty

modified theorem Set.sUnion_empty

modified theorem Set.sUnion_eq_biUnion

modified theorem Set.sUnion_eq_compl_sInter_compl

modified theorem Set.sUnion_eq_empty

modified theorem Set.sUnion_eq_iUnion

modified theorem Set.sUnion_eq_univ_iff

modified theorem Set.sUnion_iUnion

added theorem Set.sUnion_image2

modified theorem Set.sUnion_image

modified theorem Set.sUnion_insert

modified theorem Set.sUnion_pair

modified theorem Set.sUnion_range

modified theorem Set.sUnion_singleton

modified theorem Set.sUnion_subset

modified theorem Set.sUnion_subset_iff

modified theorem Set.sUnion_subset_sUnion

modified theorem Set.sUnion_union

modified theorem Set.subset_sUnion_of_mem