Partial homeomorphisms: basic theory

Main definitions

• OpenPartialHomeomorph.refl: the identity open partial homeomorphism
• Topology.IsOpenEmbedding.toOpenPartialHomeomorph: construct a partial homeomorphism from an open embedding

def OpenPartialHomeomorph.refl (X : Type u_7) [TopologicalSpace X] : OpenPartialHomeomorph X X

The identity on the whole space as an open partial homeomorphism.

Equations

• OpenPartialHomeomorph.refl X = (Homeomorph.refl X).toOpenPartialHomeomorph

@[simp]

theorem OpenPartialHomeomorph.refl_apply (X : Type u_7) [TopologicalSpace X] : ↑(OpenPartialHomeomorph.refl X) = id

theorem OpenPartialHomeomorph.refl_target (X : Type u_7) [TopologicalSpace X] : (OpenPartialHomeomorph.refl X).target = Set.univ

theorem OpenPartialHomeomorph.refl_source (X : Type u_7) [TopologicalSpace X] : (OpenPartialHomeomorph.refl X).source = Set.univ

@[simp]

theorem OpenPartialHomeomorph.refl_partialEquiv {X : Type u_1} [TopologicalSpace X] : (OpenPartialHomeomorph.refl X).toPartialEquiv = PartialEquiv.refl X

@[simp]

theorem OpenPartialHomeomorph.refl_symm {X : Type u_1} [TopologicalSpace X] : (OpenPartialHomeomorph.refl X).symm = OpenPartialHomeomorph.refl X

theorem OpenPartialHomeomorph.source_preimage_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.source ⊆ ↑e ⁻¹' e.target

theorem OpenPartialHomeomorph.image_eq_target_inter_inv_preimage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (h : s ⊆ e.source) : ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s

theorem OpenPartialHomeomorph.image_source_inter_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s

theorem OpenPartialHomeomorph.image_source_inter_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)

theorem OpenPartialHomeomorph.symm_image_eq_source_inter_preimage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set Y} (h : s ⊆ e.target) : ↑e.symm '' s = e.source ∩ ↑e ⁻¹' s

theorem OpenPartialHomeomorph.symm_image_target_inter_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) : ↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' (e.target ∩ s)

theorem OpenPartialHomeomorph.source_inter_preimage_inv_preimage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : e.source ∩ ↑e ⁻¹' ↑e.symm ⁻¹' s = e.source ∩ s

theorem OpenPartialHomeomorph.target_inter_inv_preimage_preimage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) : e.target ∩ ↑e.symm ⁻¹' ↑e ⁻¹' s = e.target ∩ s

theorem OpenPartialHomeomorph.source_inter_preimage_target_inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) : e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s

theorem OpenPartialHomeomorph.image_source_eq_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : ↑e '' e.source = e.target

theorem OpenPartialHomeomorph.symm_image_target_eq_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : ↑e.symm '' e.target = e.source

theorem OpenPartialHomeomorph.isOpen_inter_preimage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set Y} (hs : IsOpen s) : IsOpen (e.source ∩ ↑e ⁻¹' s)

theorem OpenPartialHomeomorph.isOpen_inter_preimage_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) : IsOpen (e.target ∩ ↑e.symm ⁻¹' s)

theorem OpenPartialHomeomorph.isOpen_image_of_subset_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) (hse : s ⊆ e.source) : IsOpen (↑e '' s)

An open partial homeomorphism is an open map on its source: the image of an open subset of the source is open.

theorem OpenPartialHomeomorph.isOpen_image_source_inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) : IsOpen (↑e '' (e.source ∩ s))

The image of the restriction of an open set to the source is open.

theorem OpenPartialHomeomorph.isOpen_image_symm_of_subset_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {t : Set Y} (ht : IsOpen t) (hte : t ⊆ e.target) : IsOpen (↑e.symm '' t)

The inverse of an open partial homeomorphism e is an open map on e.target.

theorem OpenPartialHomeomorph.isOpen_symm_image_iff_of_subset_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {t : Set Y} (hs : t ⊆ e.target) : IsOpen (↑e.symm '' t) ↔ IsOpen t

theorem OpenPartialHomeomorph.isOpen_image_iff_of_subset_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : s ⊆ e.source) : IsOpen (↑e '' s) ↔ IsOpen s

def OpenPartialHomeomorph.ofContinuousOpenRestrict {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.restrict ↑e)) (hs : IsOpen e.source) : OpenPartialHomeomorph X Y

A PartialEquiv with continuous open forward map and open source is a OpenPartialHomeomorph.

Equations

• OpenPartialHomeomorph.ofContinuousOpenRestrict e hc ho hs = { toPartialEquiv := e, continuousOn_toFun := hc, continuousOn_invFun := ⋯, open_source := hs, open_target := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.ofContinuousOpenRestrict_toPartialHomeomorph {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.restrict ↑e)) (hs : IsOpen e.source) : (ofContinuousOpenRestrict e hc ho hs).toPartialHomeomorph = { toPartialEquiv := e, continuousOn_toFun := hc, continuousOn_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.coe_ofContinuousOpenRestrict {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.restrict ↑e)) (hs : IsOpen e.source) : ↑(ofContinuousOpenRestrict e hc ho hs) = ↑e

@[simp]

theorem OpenPartialHomeomorph.coe_ofContinuousOpenRestrict_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.restrict ↑e)) (hs : IsOpen e.source) : ↑(ofContinuousOpenRestrict e hc ho hs).symm = ↑e.symm

def OpenPartialHomeomorph.ofContinuousOpen {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source) : OpenPartialHomeomorph X Y

A PartialEquiv with continuous open forward map and open source is a OpenPartialHomeomorph.

Equations

• OpenPartialHomeomorph.ofContinuousOpen e hc ho hs = OpenPartialHomeomorph.ofContinuousOpenRestrict e hc ⋯ hs

@[simp]

theorem OpenPartialHomeomorph.ofContinuousOpen_toPartialHomeomorph {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source) : (ofContinuousOpen e hc ho hs).toPartialHomeomorph = { toPartialEquiv := e, continuousOn_toFun := hc, continuousOn_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.coe_ofContinuousOpen {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source) : ↑(ofContinuousOpen e hc ho hs) = ↑e

@[simp]

theorem OpenPartialHomeomorph.coe_ofContinuousOpen_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source) : ↑(ofContinuousOpen e hc ho hs).symm = ↑e.symm

def OpenPartialHomeomorph.homeomorphOfImageSubsetSource {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) : ↑s ≃ₜ ↑t

The homeomorphism obtained by restricting an OpenPartialHomeomorph to a subset of the source.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OpenPartialHomeomorph.homeomorphOfImageSubsetSource_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) (a✝ : ↑s) : (e.homeomorphOfImageSubsetSource hs ht) a✝ = Set.MapsTo.restrict (↑e) s t ⋯ a✝

@[simp]

theorem OpenPartialHomeomorph.homeomorphOfImageSubsetSource_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) (a✝ : ↑t) : (e.homeomorphOfImageSubsetSource hs ht).symm a✝ = Set.MapsTo.restrict (↑e.symm) t s ⋯ a✝

def OpenPartialHomeomorph.toHomeomorphSourceTarget {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : ↑e.source ≃ₜ ↑e.target

An open partial homeomorphism defines a homeomorphism between its source and target.

Equations

• e.toHomeomorphSourceTarget = e.homeomorphOfImageSubsetSource ⋯ ⋯

@[simp]

theorem OpenPartialHomeomorph.toHomeomorphSourceTarget_apply_coe {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (a✝ : ↑e.source) : ↑(e.toHomeomorphSourceTarget a✝) = ↑e ↑a✝

@[simp]

theorem OpenPartialHomeomorph.toHomeomorphSourceTarget_symm_apply_coe {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (a✝ : ↑e.target) : ↑(e.toHomeomorphSourceTarget.symm a✝) = ↑e.symm ↑a✝

theorem OpenPartialHomeomorph.secondCountableTopology_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) [SecondCountableTopology Y] : SecondCountableTopology ↑e.source

theorem OpenPartialHomeomorph.nhds_eq_comap_inf_principal {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : nhds x = Filter.comap (↑e) (nhds (↑e x)) ⊓ Filter.principal e.source

def OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ) : X ≃ₜ Y

If an open partial homeomorphism has source and target equal to univ, then it induces a homeomorphism between the whole spaces, expressed in this definition.

Equations

• e.toHomeomorphOfSourceEqUnivTargetEqUniv h h' = { toFun := ↑e, invFun := ↑e.symm, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ) : ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h') = ↑e

@[simp]

theorem OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ) : ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h').symm = ↑e.symm

theorem OpenPartialHomeomorph.isOpenEmbedding_restrict {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : Topology.IsOpenEmbedding (e.source.restrict ↑e)

theorem OpenPartialHomeomorph.to_isOpenEmbedding {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (h : e.source = Set.univ) : Topology.IsOpenEmbedding ↑e

An open partial homeomorphism whose source is all of X defines an open embedding of X into Y. The converse is also true; see IsOpenEmbedding.toOpenPartialHomeomorph.

Open embeddings

noncomputable def Topology.IsOpenEmbedding.toOpenPartialHomeomorph {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] : OpenPartialHomeomorph X Y

An open embedding of X into Y, with X nonempty, defines an open partial homeomorphism whose source is all of X. The converse is also true; see OpenPartialHomeomorph.to_isOpenEmbedding.

Equations

• Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h = OpenPartialHomeomorph.ofContinuousOpen (Set.InjOn.toPartialEquiv f Set.univ ⋯) ⋯ ⋯ ⋯

@[simp]

theorem Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] : (toOpenPartialHomeomorph f h).target = Set.range f

@[simp]

theorem Topology.IsOpenEmbedding.toOpenPartialHomeomorph_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] : (toOpenPartialHomeomorph f h).source = Set.univ

@[simp]

theorem Topology.IsOpenEmbedding.toOpenPartialHomeomorph_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] : ↑(toOpenPartialHomeomorph f h) = f

theorem Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] {x : X} : ↑(toOpenPartialHomeomorph f h).symm (f x) = x

theorem Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] {x : Y} (hx : x ∈ Set.range f) : f (↑(toOpenPartialHomeomorph f h).symm x) = x

inclusion of an open set in a topological space

noncomputable def TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) : OpenPartialHomeomorph (↥s) X

The inclusion of an open subset s of a space X into X is an open partial homeomorphism from the subtype s to X.

Equations

• s.openPartialHomeomorphSubtypeCoe hs = Topology.IsOpenEmbedding.toOpenPartialHomeomorph Subtype.val ⋯

@[simp]

theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_coe {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) : ↑(s.openPartialHomeomorphSubtypeCoe hs) = Subtype.val

@[simp]

theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) : (s.openPartialHomeomorphSubtypeCoe hs).source = Set.univ

@[simp]

theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) : (s.openPartialHomeomorphSubtypeCoe hs).target = ↑s