mathlib

ad4aca0c - feat(topology/local_homeomorph): add `is_image`, `piecewise`, and `disjoint_union` (#6804)

feat(topology/local_homeomorph): add `is_image`, `piecewise`, and `disjoint_union` (#6804) Also add `local_equiv.copy` and `local_homeomorph.replace_equiv` and use them for `local_equiv.disjoint_union` and `local_homeomorph.disjoint_union.