English
Given a Homeomorph e: X ≃ₜ Y and an open s ⊆ X with e''s image equal to t ⊆ Y, there exists an OpenPartialHomeomorph X Y whose partial equiv is the restriction of e to s and t, with open_source = s and open_target = t, and continuousOn_toFun/continuousOn_invFun matching e.
Русский
Пусть e: X ≃ₜ Y — гомеоморфизм, s ⊆ X открыто, t ⊆ Y открыто и e[s] = t. Тогда существует OpenPartialHomeomorph X Y, чьё частичное эквивалентное отображение является ограничением e до s и t, source = s, target = t, и непрерывности соответствуют e и e^{-1}.
LaTeX
$$\( \exists e' : OpenPartialHomeomorph X Y,\ e'.toPartialEquiv = e.toPartialEquivOfImageEq s t h,\ open_source := hs,\ open_target := by simpa [← h],\ continuousOn_toFun := e.continuous.continuousOn,\ continuousOn_invFun := e.symm.continuous.continuousOn.\)$$
Lean4
/-- Interpret a `Homeomorph` as an `OpenPartialHomeomorph` by restricting it
to an open set `s` in the domain and to `t` in the codomain. -/
@[simps! -fullyApplied apply symm_apply toPartialEquiv, simps! -isSimp source target]
def _root_.Homeomorph.toOpenPartialHomeomorphOfImageEq (e : X ≃ₜ Y) (s : Set X) (hs : IsOpen s) (t : Set Y)
(h : e '' s = t) : OpenPartialHomeomorph X Y
where
toPartialEquiv := e.toPartialEquivOfImageEq s t h
open_source := hs
open_target := by simpa [← h]
continuousOn_toFun := e.continuous.continuousOn
continuousOn_invFun := e.symm.continuous.continuousOn
