Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-28 18:56 35f0f1ba

View on Github →

feat(data/set/basic): Refactor and additions of sep lemmas (#16566) Add and refactor sep lemmas.

Estimated changes

Modified src/analysis/convex/quasiconvex.lean

Modified src/data/set/basic.lean

deleted theorem set.eq_sep_of_subset

deleted theorem set.forall_not_of_sep_empty

modified theorem set.mem_sep

modified theorem set.mem_sep_iff

added theorem set.sep_and

modified theorem set.sep_empty

added theorem set.sep_eq_empty_iff_mem_false

added theorem set.sep_eq_of_subset

added theorem set.sep_eq_self_iff_mem_true

added theorem set.sep_ext_iff

modified theorem set.sep_false

added theorem set.sep_inter

deleted theorem set.sep_inter_sep

modified theorem set.sep_mem_eq

added theorem set.sep_or

modified theorem set.sep_set_of

modified theorem set.sep_true

added theorem set.sep_union

modified theorem set.sep_univ

Modified src/data/set/finite.lean