Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-04 17:34 35b835a2

View on Github →

feat(data/set/sigma): Indexed sum of sets (#12305) Define set.sigma, the sum of a family of sets indexed by a set.

Estimated changes

added theorem finset.coe_sigma
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.insert_sigma
added theorem set.mem_sigma_iff
added theorem set.mk_mem_sigma
added theorem set.mk_preimage_sigma
added theorem set.mk_sigma_iff
added theorem set.nonempty.sigma_fst
added theorem set.nonempty.sigma_snd
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_singleton
added theorem set.sigma_subset_iff
added theorem set.sigma_union
added theorem set.sigma_univ
added theorem set.singleton_sigma
added theorem set.union_sigma
added theorem set.univ_sigma_univ
modified theorem imp_iff_not_or
added theorem imp_iff_or_not
modified theorem not_or_of_imp
added theorem or_not_of_imp