English
Restricting an open partial homeomorphism e to e.source ∩ s with s open yields an OpenPartialHomeomorph.
Русский
Ограничение открытого частичного гомоморфизма e до e.source ∩ s, где s открыто, даёт новый OpenPartialHomeomorph.
LaTeX
$$$\\text{restrOpen }(s, hs): OpenPartialHomeomorph\\ X\\ Y$ with source $e.source \\cap s$ and target $e.target \\cap s$$$
Lean4
/-- Restricting an open partial homeomorphism `e` to `e.source ∩ s` when `s` is open.
This is sometimes hard to use because of the openness assumption, but it has the advantage that
when it can be used then its `PartialEquiv` is defeq to `PartialEquiv.restr`. -/
protected def restrOpen (s : Set X) (hs : IsOpen s) : OpenPartialHomeomorph X Y :=
(@IsImage.of_symm_preimage_eq X Y _ _ e s (e.symm ⁻¹' s) rfl).restr (IsOpen.inter e.open_source hs)
