English
The restriction of an OpenPartialHomeomorph to its source yields an open embedding; in particular, the restriction is an open map and injective.
Русский
Ограничение OpenPartialHomeomorph к его источнику образует открытое вложение; ограничение отображаетOPEN-образ и инъективно.
LaTeX
$$$IsOpenEmbedding (e.source.restrict e.toFun')$$
Lean4
/-- The homeomorphism obtained by restricting an `OpenPartialHomeomorph` to a subset of the source.
-/
@[simps]
def homeomorphOfImageSubsetSource {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : e '' s = t) : s ≃ₜ t :=
have h₁ : MapsTo e s t := mapsTo_iff_image_subset.2 ht.subset
have h₂ : t ⊆ e.target := ht ▸ e.image_source_eq_target ▸ image_mono hs
have h₃ : MapsTo e.symm t s := ht ▸ forall_mem_image.2 fun _x hx => (e.left_inv (hs hx)).symm ▸ hx
{ toFun := MapsTo.restrict e s t h₁
invFun := MapsTo.restrict e.symm t s h₃
left_inv := fun a => Subtype.ext (e.left_inv (hs a.2))
right_inv := fun b => Subtype.eq <| e.right_inv (h₂ b.2)
continuous_toFun := (e.continuousOn.mono hs).mapsToRestrict h₁
continuous_invFun := (e.continuousOn_symm.mono h₂).mapsToRestrict h₃ }
