Partial homeomorphisms: basic theory

Main definitions

• PartialHomeomorph.refl: the identity partial homeomorphism
• IsEmbedding.toPartialHomeomorph: an embedding of X into Y, with X nonempty, defines a partial homeomorphism whose source is all of X.

def PartialHomeomorph.refl (X : Type u_3) [TopologicalSpace X] : PartialHomeomorph X X

The identity on the whole space as a partial homeomorphism.

Equations

• PartialHomeomorph.refl X = (Homeomorph.refl X).toPartialHomeomorph

@[simp]

theorem PartialHomeomorph.refl_apply (X : Type u_3) [TopologicalSpace X] : ↑(PartialHomeomorph.refl X) = id

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

def PartialHomeomorph.ofContinuousOpenRestrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)) : PartialHomeomorph X Y

A PartialEquiv which is continuous on its source and has open forward map (on its source) is a PartialHomeomorph.

Equations

• PartialHomeomorph.ofContinuousOpenRestrict e hc ho = { toPartialEquiv := e, continuousOn_toFun := hc, continuousOn_invFun := ⋯ }

@[simp]

theorem PartialHomeomorph.ofContinuousOpenRestrict_toPartialEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)) : (ofContinuousOpenRestrict e hc ho).toPartialEquiv = e

@[simp]

theorem PartialHomeomorph.coe_ofContinuousOpenRestrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)) : ↑(ofContinuousOpenRestrict e hc ho) = ↑e

@[simp]

theorem PartialHomeomorph.coe_ofContinuousOpenRestrict_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)) : ↑(ofContinuousOpenRestrict e hc ho).symm = ↑e.symm

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

A PartialEquiv which is continuous on its source and has open forward map (on its source) and open source is a PartialHomeomorph.

Equations

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

@[simp]

theorem PartialHomeomorph.ofContinuousOpen_toPartialEquiv {X : Type u_1} {Y : Type u_2} [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).toPartialEquiv = e

@[simp]

theorem PartialHomeomorph.coe_ofContinuousOpen {X : Type u_1} {Y : Type u_2} [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 PartialHomeomorph.coe_ofContinuousOpen_symm {X : Type u_1} {Y : Type u_2} [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 PartialHomeomorph.homeomorphOfImageSubsetSource {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) : ↑s ≃ₜ ↑t

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

Equations

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

@[simp]

theorem PartialHomeomorph.homeomorphOfImageSubsetSource_symm_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph 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✝

@[simp]

theorem PartialHomeomorph.homeomorphOfImageSubsetSource_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph 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✝

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

A partial homeomorphism defines a homeomorphism between its source and target.

Equations

• e.toHomeomorphSourceTarget = e.homeomorphOfImageSubsetSource ⋯ ⋯

@[simp]

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

@[simp]

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

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

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

If a 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 PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ) : ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h') = ↑e

@[simp]

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

theorem PartialHomeomorph.isEmbedding_restrict {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Topology.IsEmbedding (e.source.domRestrict ↑e.toPartialEquiv)

theorem PartialHomeomorph.isEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (h : e.source = Set.univ) : Topology.IsEmbedding ↑e

A partial homeomorphism whose source is all of X defines an embedding of X into Y. The converse is also true; see IsEmbedding.toPartialHomeomorph.

def PartialHomeomorph.ofIsHomeomorphToEquiv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : PartialEquiv X Y) (h : IsHomeomorph ⇑f.toEquiv) : PartialHomeomorph X Y

If a PartialEquiv is a homeomorphism when restricted to source and target, then it is a PartialHomeomorph.

Equations

• PartialHomeomorph.ofIsHomeomorphToEquiv f h = { toPartialEquiv := f, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

Embeddings

noncomputable def Topology.IsEmbedding.toPartialHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsEmbedding f) [Nonempty X] : PartialHomeomorph X Y

An embedding of X into Y, with X nonempty, defines a partial homeomorphism whose source is all of X. The converse is also true; see PartialHomeomorph.isEmbedding.

Equations

• Topology.IsEmbedding.toPartialHomeomorph f h = PartialHomeomorph.ofIsHomeomorphToEquiv (Set.InjOn.toPartialEquiv f Set.univ ⋯) ⋯

@[simp]

theorem Topology.IsEmbedding.toPartialHomeomorph_source {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsEmbedding f) [Nonempty X] : (toPartialHomeomorph f h).source = Set.univ

@[simp]

theorem Topology.IsEmbedding.toPartialHomeomorph_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsEmbedding f) [Nonempty X] : ↑(toPartialHomeomorph f h) = f

@[simp]

theorem Topology.IsEmbedding.toPartialHomeomorph_target {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsEmbedding f) [Nonempty X] : (toPartialHomeomorph f h).target = Set.range f

theorem Topology.IsEmbedding.toPartialHomeomorph_left_inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsEmbedding f) [Nonempty X] {x : X} : ↑(toPartialHomeomorph f h).symm (f x) = x

theorem Topology.IsEmbedding.toPartialHomeomorph_right_inv {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsEmbedding f) [Nonempty X] {x : Y} (hx : x ∈ Set.range f) : f (↑(toPartialHomeomorph f h).symm x) = x

inclusion of a set in a topological space

noncomputable def Set.partialHomeomorphSubtypeCoe {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : Nonempty ↑s) : PartialHomeomorph (↑s) X

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

Equations

• s.partialHomeomorphSubtypeCoe hs = Topology.IsEmbedding.toPartialHomeomorph Subtype.val ⋯

@[simp]

theorem Set.partialHomeomorphSubtypeCoe_coe {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : Nonempty ↑s) : ↑(s.partialHomeomorphSubtypeCoe hs) = Subtype.val

@[simp]

theorem Set.partialHomeomorphSubtypeCoe_source {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : Nonempty ↑s) : (s.partialHomeomorphSubtypeCoe hs).source = univ

@[simp]

theorem Set.partialHomeomorphSubtypeCoe_target {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : Nonempty ↑s) : (s.partialHomeomorphSubtypeCoe hs).target = s