local_equiv): define `piecewise` and `disjoint_union` (#6700)

Commit

4 years ago

feat(data/equiv/local_equiv): define `piecewise` and `disjoint_union` (#6700) Also change some lemmas to use `set.ite`.

Author

urkud

Parents