Lean4
/-- Combine two `OpenPartialHomeomorph`s with disjoint sources and disjoint targets. We reuse
`OpenPartialHomeomorph.piecewise` then override `toPartialEquiv` to `PartialEquiv.disjointUnion`.
This way we have better definitional equalities for `source` and `target`. -/
def disjointUnion (e e' : OpenPartialHomeomorph X Y) [∀ x, Decidable (x ∈ e.source)] [∀ y, Decidable (y ∈ e.target)]
(Hs : Disjoint e.source e'.source) (Ht : Disjoint e.target e'.target) : OpenPartialHomeomorph X Y :=
(e.piecewise e' e.source e.target e.isImage_source_target (e'.isImage_source_target_of_disjoint e Hs.symm Ht.symm)
(by rw [e.open_source.inter_frontier_eq, (Hs.symm.frontier_right e'.open_source).inter_eq])
(by
rw [e.open_source.inter_frontier_eq]
exact eqOn_empty _ _)).replaceEquiv
(e.toPartialEquiv.disjointUnion e'.toPartialEquiv Hs Ht) (PartialEquiv.disjointUnion_eq_piecewise _ _ _ _).symm
