Lean4
/-- Combine two `PartialEquiv`s using `Set.piecewise`. The source of the new `PartialEquiv` 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. The definition assumes `e.isImage s t` and
`e'.isImage s t`. -/
@[simps -fullyApplied]
def piecewise (e e' : PartialEquiv α β) (s : Set α) (t : Set β) [∀ x, Decidable (x ∈ s)] [∀ y, Decidable (y ∈ t)]
(H : e.IsImage s t) (H' : e'.IsImage s t) : PartialEquiv α β
where
toFun := s.piecewise e e'
invFun := t.piecewise e.symm e'.symm
source := s.ite e.source e'.source
target := t.ite e.target e'.target
map_source' := H.mapsTo.piecewise_ite H'.compl.mapsTo
map_target' := H.symm.mapsTo.piecewise_ite H'.symm.compl.mapsTo
left_inv' := H.leftInvOn_piecewise H'
right_inv' := H.symm.leftInvOn_piecewise H'.symm
