Commit 2022-12-14 03:08 c818a43d

View on Github →

feat port: data.set.sigma (#982) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Sigma.lean

added theorem Set.Nonempty.sigma_fst

added theorem Set.Nonempty.sigma_snd

added theorem Set.empty_sigma

added theorem Set.exists_sigma_iff

added theorem Set.forall_sigma_iff

added theorem Set.fst_image_sigma

added theorem Set.fst_image_sigma_subset

added theorem Set.image_sigmaMk_preimage_sigmaMap

added theorem Set.image_sigmaMk_preimage_sigmaMap_subset

added theorem Set.image_sigmaMk_subset_sigma_left

added theorem Set.image_sigmaMk_subset_sigma_right

added theorem Set.insert_sigma

added theorem Set.mem_sigma_iff

added theorem Set.mk_mem_sigma

added theorem Set.mk_preimage_sigma

added theorem Set.mk_preimage_sigma_eq_empty

added theorem Set.mk_preimage_sigma_eq_if

added theorem Set.mk_preimage_sigma_fn_eq_if

added theorem Set.mk_sigma_iff

added theorem Set.preimage_image_sigmaMk_of_ne

added theorem Set.preimage_sigmaMap_sigma

added theorem Set.range_sigmaMk

added theorem Set.sigma_diff_sigma

added theorem Set.sigma_empty

added theorem Set.sigma_eq_empty_iff

added theorem Set.sigma_insert

added theorem Set.sigma_inter_sigma

added theorem Set.sigma_mono

added theorem Set.sigma_nonempty_iff

added theorem Set.sigma_preimage_eq

added theorem Set.sigma_preimage_left

added theorem Set.sigma_preimage_right

added theorem Set.sigma_singleton

added theorem Set.sigma_subset_iff

added theorem Set.sigma_subset_preimage_fst

added theorem Set.sigma_union

added theorem Set.sigma_univ

added theorem Set.sigma_univ_range_eq

added theorem Set.singleton_sigma

added theorem Set.singleton_sigma_singleton

added theorem Set.union_sigma

added theorem Set.univ_sigma_univ