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.

source

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

PartialHomeomorph X X

The identity on the whole space as a partial homeomorphism.

Instances For

source

@[simp]

theorem PartialHomeomorph.refl_apply (X : Type u_3) [TopologicalSpace X] :

↑(PartialHomeomorph.refl X) = id

source

theorem PartialHomeomorph.refl_target (X : Type u_3) [TopologicalSpace X] :

(PartialHomeomorph.refl X).target = Set.univ

source

theorem PartialHomeomorph.refl_source (X : Type u_3) [TopologicalSpace X] :

(PartialHomeomorph.refl X).source = Set.univ

source

@[simp]

theorem PartialHomeomorph.refl_partialEquiv {X : Type u_1} [TopologicalSpace X] :

(PartialHomeomorph.refl X).toPartialEquiv = PartialEquiv.refl X

source

@[simp]

theorem PartialHomeomorph.refl_symm {X : Type u_1} [TopologicalSpace X] :

(PartialHomeomorph.refl X).symm = PartialHomeomorph.refl X

source

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

source

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

source

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

source

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)

source

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

source

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)

source

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

source

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

source

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

source

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

source

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

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.

Instances For

source

@[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

source

@[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

source

@[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

source

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.

Instances For

source

@[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

source

@[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

source

@[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

source

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.

Instances For

source

@[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✝

source

@[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✝

source

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.

Instances For

source

@[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✝

source

@[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✝

source

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

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.

Instances For

source

@[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

source

@[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

source

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)

source

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.

source

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.

Instances For

Embeddings #

source

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.

Instances For

source

@[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

source

@[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

source

@[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

source

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

source

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

source

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.

Instances For

source

@[simp]

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

↑(s.partialHomeomorphSubtypeCoe hs) = Subtype.val

source

@[simp]

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

(s.partialHomeomorphSubtypeCoe hs).source = univ

source

@[simp]

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

(s.partialHomeomorphSubtypeCoe hs).target = s

Documentation

Mathlib.Topology.PartialHomeomorph.Basic

Partial homeomorphisms: basic theory #

Main definitions #

Embeddings #