English
Let e be an open partial homeomorphism between spaces X and Y. If s ⊆ X and t ⊆ Y satisfy that e maps s onto t (e.IsImage s t) and e.source ∩ s is open, then the restriction of e to these corresponding open regions is again an open partial homeomorphism X ⇔ Y, with source e.source ∩ s and target e.target ∩ t, given by restricting the forward and inverse maps accordingly.
Русский
Пусть e — открытое частичное гомоморфизм между пространствами X и Y. Если пары подмножеств s ⊆ X, t ⊆ Y удовлетворяют условию, что e отображает s в t (e.IsImage s t) и e.source ∩ s открыто, то ограничение e на соответствующих открытых областях снова является открытым частичным гомоморфизмом X ⇔ Y с источником e.source ∩ s и образом e.target ∩ t, получаемым ограничением отображения вперед и обратного отображения.
LaTeX
$$$\\forall \\{X,Y\\}, \\forall e: OpenPartialHomeomorph\\ X\\ Y,\\; \\forall s\\subset X, t\\subset Y,\\; e.IsImage\\ s\\ t \\wedge IsOpen (e.source \\cap s) \\Rightarrow \\text{OpenPartialHomeomorph } e.restr\\ h\\ hs$$$
Lean4
/-- Restrict an `OpenPartialHomeomorph` to a pair of corresponding open sets. -/
@[simps toPartialEquiv]
def restr (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) : OpenPartialHomeomorph X Y
where
toPartialEquiv := h.toPartialEquiv.restr
open_source := hs
open_target := h.isOpen_iff.1 hs
continuousOn_toFun := e.continuousOn.mono inter_subset_left
continuousOn_invFun := e.symm.continuousOn.mono inter_subset_left
