Mathlib v3 is deprecated. Go to Mathlib v4

Def local_equiv.disjoint_union

Modification history

2022-05-24 16:46
src/logic/equiv/local_equiv.lean
feat(topology/local_homeomorph): define helper definition (#14360) …
Modified local_equiv.disjoint_unionView on Github →
2021-03-18 23:42
src/data/equiv/local_equiv.lean
feat(data/equiv/local_equiv): define `piecewise` and `disjoint_union` (#6700) …
Added local_equiv.disjoint_unionView on Github →