Lean4
/-- Combine two `OpenPartialHomeomorph`s using `Set.piecewise`. The source of the new
`OpenPartialHomeomorph` is `s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s`, and similarly
for target. The function sends `e.source ∩ s` to `e.target ∩ t` using `e` and
`e'.source \ s` to `e'.target \ t` using `e'`, and similarly for the inverse function.
To ensure the maps `toFun` and `invFun` are inverse of each other on the new `source` and `target`,
the definition assumes that the sets `s` and `t` are related both by `e.is_image` and `e'.is_image`.
To ensure that the new maps are continuous on `source`/`target`, it also assumes that `e.source` and
`e'.source` meet `frontier s` on the same set and `e x = e' x` on this intersection. -/
@[simps! -fullyApplied toPartialEquiv apply]
def piecewise (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [∀ x, Decidable (x ∈ s)]
[∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t)
(Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : EqOn e e' (e.source ∩ frontier s)) :
OpenPartialHomeomorph X Y
where
toPartialEquiv := e.toPartialEquiv.piecewise e'.toPartialEquiv s t H H'
open_source := e.open_source.ite e'.open_source Hs
open_target := e.open_target.ite e'.open_target <| H.frontier.inter_eq_of_inter_eq_of_eqOn H'.frontier Hs Heq
continuousOn_toFun := continuousOn_piecewise_ite e.continuousOn e'.continuousOn Hs Heq
continuousOn_invFun :=
continuousOn_piecewise_ite e.continuousOn_symm e'.continuousOn_symm
(H.frontier.inter_eq_of_inter_eq_of_eqOn H'.frontier Hs Heq) (H.frontier.symm_eqOn_of_inter_eq_of_eqOn Hs Heq)
