Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-06 21:16 b280b005

View on Github →

feat(data/set/basic): add set.set_ite (#6557) I'm going to use it as source and target in local_equiv.piecewise and local_homeomorph.piecewise. There are many non-defeq ways to define this set and I think that it's better to have a name than to ensure that we always use the same formula.

Estimated changes

added theorem set.diff_univ
added theorem set.inter_subset_ite
added theorem set.ite_compl
added theorem set.ite_diff_self
added theorem set.ite_empty
added theorem set.ite_inter
added theorem set.ite_inter_inter
added theorem set.ite_inter_self
added theorem set.ite_mono
added theorem set.ite_same
added theorem set.ite_subset_union
added theorem set.ite_univ