Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-01 22:10 777f6b40

View on Github →

feat(data/set/basic): add some more set lemmas

Estimated changes

Modified data/analysis/filter.lean

Modified data/set/basic.lean

added theorem set.compl_subset_comm

added theorem set.compl_subset_iff_union

deleted theorem set.compl_subset_of_compl_subset

modified theorem set.compl_union_self

modified theorem set.eq_empty_of_subset_empty

modified theorem set.eq_univ_of_univ_subset

modified theorem set.exists_mem_of_ne_empty

added theorem set.image_compl_eq

added theorem set.image_compl_subset

modified theorem set.image_empty

modified theorem set.image_inter

added theorem set.image_univ_of_surjective

added theorem set.mem_compl_image

deleted theorem set.mem_image_compl

modified theorem set.mem_univ

deleted theorem set.mem_univ_eq

deleted theorem set.mem_univ_iff

added theorem set.subset.antisymm_iff

added theorem set.subset_compl_comm

added theorem set.subset_compl_iff_disjoint

added theorem set.subset_image_compl

modified theorem set.union_compl_self

added theorem set.univ_subset_iff