English
A PartialEquiv with a continuous open forward map and open source yields an OpenPartialHomeomorph when restricted to an open subset.
Русский
Частичное эквивалентное отображение с непрерывной открытой отображающей картой и открытым источником можно сделать открытым частичным гомоморфизмом при ограничении на открытое множество.
LaTeX
$$$e: PartialEquiv\\ X\\ Y,\\; hc: ContinuousOn\\ e\\ e.source,\\; ho: IsOpenMap\\ e,\\; hs: IsOpen\\ e.source \\Rightarrow OpenPartialHomeomorph\\ X\\ Y$$$
Lean4
/-- A `PartialEquiv` with continuous open forward map and open source is a
`OpenPartialHomeomorph`. -/
def ofContinuousOpenRestrict (e : PartialEquiv X Y) (hc : ContinuousOn e e.source)
(ho : IsOpenMap (e.source.restrict e)) (hs : IsOpen e.source) : OpenPartialHomeomorph X Y
where
toPartialEquiv := e
open_source := hs
open_target := by simpa only [range_restrict, e.image_source_eq_target] using ho.isOpen_range
continuousOn_toFun := hc
continuousOn_invFun := e.image_source_eq_target ▸ ho.continuousOn_image_of_leftInvOn e.leftInvOn
