Documentation

Mathlib.Topology.OpenPartialHomeomorph.Basic

Partial homeomorphisms: basic theory #

Main definitions #

OpenPartialHomeomorph.refl: the identity open partial homeomorphism
Topology.IsOpenEmbedding.toOpenPartialHomeomorph: construct an open 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

Instances For

@[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.domRestrict ↑e)) (hs : IsOpen e.source) :

OpenPartialHomeomorph X Y

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

Equations

OpenPartialHomeomorph.ofContinuousOpenRestrict e hc ho hs = { toPartialHomeomorph := PartialHomeomorph.ofContinuousOpenRestrict e hc ho, open_source := hs, open_target := ⋯ }

Instances For

@[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.domRestrict ↑e)) (hs : IsOpen e.source) :

(ofContinuousOpenRestrict e hc ho hs).toPartialHomeomorph = PartialHomeomorph.ofContinuousOpenRestrict e hc ho

@[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.domRestrict ↑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.domRestrict ↑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 which is continuous on its source and has open forward map (on its source) and open source is an OpenPartialHomeomorph.

Equations

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

Instances For

@[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 = PartialHomeomorph.ofContinuousOpenRestrict e hc ⋯

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

e.homeomorphOfImageSubsetSource hs ht = e.homeomorphOfImageSubsetSource hs ht

Instances For

@[simp]

theorem OpenPartialHomeomorph.homeomorphOfImageSubsetSource_symm_apply_coe {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✝) = ↑e.symm ↑a✝

@[simp]

theorem OpenPartialHomeomorph.homeomorphOfImageSubsetSource_apply_coe {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✝) = ↑e ↑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 ⋯ ⋯

Instances For

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

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' = e.toHomeomorphOfSourceEqUnivTargetEqUniv h h'

Instances For

@[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.domRestrict ↑e)

theorem OpenPartialHomeomorph.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.

@[deprecated OpenPartialHomeomorph.isOpenEmbedding (since := "2026-07-17")]

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

Alias of OpenPartialHomeomorph.isOpenEmbedding.

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.isOpenEmbedding.

Equations

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

Instances For

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

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

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 ⋯

Instances For

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