mathlib3
b280b005 - feat(data/set/basic): add `set.set_ite` (#6557)

Commit
4 years ago
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. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Author
Parents
Loading