Partial homeomorphisms: definitions

This file defines homeomorphisms between subsets of topological spaces. An element e of PartialHomeomorph X Y is an extension of PartialEquiv X Y, i.e., it is a pair of functions e.toFun and e.invFun, inverse of each other on the sets e.source and e.target. Additionally, we require that the functions are continuous on them. Equivalently, they are homeomorphisms there.

As for Equivs, we register a coercion to functions, and we use e x and e.symm x throughout instead of e.toFun x and e.invFun x.

Main definitions

This file is intentionally kept small; many other constructions of, and lemmas about, partial homeomorphisms can be found in other files under Mathlib/Topology/PartialHomeomorph/.

• Homeomorph.toPartialHomeomorph: associating a partial homeomorphism to a homeomorphism, with source = target = Set.univ;
• PartialHomeomorph.symm: the inverse of a partial homeomorphism

Implementation notes

Most statements are copied from their PartialEquiv versions, although some care is required.

For design notes, see PartialEquiv.lean.

Local coding conventions

If a lemma deals with the intersection of a set with either source or target of a PartialEquiv, then it should use e.source ∩ s or e.target ∩ t, not s ∩ e.source or t ∩ e.target.

structure PartialHomeomorph (X : Type u_7) (Y : Type u_8) [TopologicalSpace X] [TopologicalSpace Y] extends PartialEquiv X Y : Type (max u_7 u_8)

Partial homeomorphisms, defined on subsets of the space

• toFun : X → Y
• invFun : Y → X
• source : Set X
• target : Set Y
• map_source' ⦃x : X⦄ : x ∈ self.source → ↑self.toPartialEquiv x ∈ self.target
• map_target' ⦃x : Y⦄ : x ∈ self.target → self.invFun x ∈ self.source
• left_inv' ⦃x : X⦄ : x ∈ self.source → self.invFun (↑self.toPartialEquiv x) = x
• right_inv' ⦃x : Y⦄ : x ∈ self.target → ↑self.toPartialEquiv (self.invFun x) = x
• continuousOn_toFun : ContinuousOn (↑self.toPartialEquiv) self.source
• continuousOn_invFun : ContinuousOn self.invFun self.target

Basic properties; inverse (symm instance)

def PartialHomeomorph.toFun' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : X → Y

Coercion of a partial homeomorphisms to a function. We don't use e.toFun because it is actually e.toPartialEquiv.toFun, so simp will apply lemmas about toPartialEquiv.

Equations

• ↑e = ↑e.toPartialEquiv

@[implicit_reducible]

instance PartialHomeomorph.instCoeFunForall {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : CoeFun (PartialHomeomorph X Y) fun (x : PartialHomeomorph X Y) => X → Y

Coercion of a PartialHomeomorph to function. Note that a PartialHomeomorph is not DFunLike.

Equations

• PartialHomeomorph.instCoeFunForall = { coe := fun (e : PartialHomeomorph X Y) => ↑e }

def PartialHomeomorph.symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : PartialHomeomorph Y X

The inverse of a partial homeomorphism

Equations

• e.symm = { toPartialEquiv := e.symm, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

def PartialHomeomorph.Simps.apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : X → Y

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations

• PartialHomeomorph.Simps.apply e = ↑e

def PartialHomeomorph.Simps.symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Y → X

See Note [custom simps projection]

Equations

• PartialHomeomorph.Simps.symm_apply e = ↑e.symm

theorem PartialHomeomorph.continuousOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : ContinuousOn (↑e) e.source

theorem PartialHomeomorph.continuousOn_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : ContinuousOn (↑e.symm) e.target

@[simp]

theorem PartialHomeomorph.coe_mk {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target) : ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ } = ↑e

@[simp]

theorem PartialHomeomorph.coe_mk_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (h₁ : ContinuousOn (↑e) e.source) (h₂ : ContinuousOn e.invFun e.target) : ↑{ toPartialEquiv := e, continuousOn_toFun := h₁, continuousOn_invFun := h₂ }.symm = ↑e.symm

theorem PartialHomeomorph.toPartialEquiv_injective {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : Function.Injective toPartialEquiv

@[simp]

theorem PartialHomeomorph.toFun_eq_coe {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : ↑e.toPartialEquiv = ↑e

@[simp]

theorem PartialHomeomorph.invFun_eq_coe {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : e.invFun = ↑e.symm

@[simp]

theorem PartialHomeomorph.coe_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : ↑e.toPartialEquiv = ↑e

@[simp]

theorem PartialHomeomorph.coe_toPartialEquiv_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : ↑e.symm = ↑e.symm

@[simp]

theorem PartialHomeomorph.map_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : X} (h : x ∈ e.source) : ↑e x ∈ e.target

theorem PartialHomeomorph.image_source_subset {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : ↑e '' e.source ⊆ e.target

Variant of map_source, stated in terms of subsets.

@[simp]

theorem PartialHomeomorph.map_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : Y} (h : x ∈ e.target) : ↑e.symm x ∈ e.source

@[simp]

theorem PartialHomeomorph.left_inv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : X} (h : x ∈ e.source) : ↑e.symm (↑e x) = x

@[simp]

theorem PartialHomeomorph.right_inv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : Y} (h : x ∈ e.target) : ↑e (↑e.symm x) = x

theorem PartialHomeomorph.eq_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : X} {y : Y} (hx : x ∈ e.source) (hy : y ∈ e.target) : x = ↑e.symm y ↔ ↑e x = y

theorem PartialHomeomorph.mapsTo {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Set.MapsTo (↑e) e.source e.target

theorem PartialHomeomorph.mapsTo_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Set.MapsTo (↑e.symm) e.target e.source

theorem PartialHomeomorph.leftInvOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Set.LeftInvOn (↑e.symm) (↑e) e.source

theorem PartialHomeomorph.rightInvOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Set.RightInvOn (↑e.symm) (↑e) e.target

theorem PartialHomeomorph.invOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Set.InvOn (↑e.symm) (↑e) e.source e.target

theorem PartialHomeomorph.injOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Set.InjOn (↑e) e.source

theorem PartialHomeomorph.bijOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Set.BijOn (↑e) e.source e.target

theorem PartialHomeomorph.surjOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Set.SurjOn (↑e) e.source e.target

def Homeomorph.toPartialHomeomorphOfImageEq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (t : Set Y) (h : ⇑e '' s = t) : PartialHomeomorph X Y

Interpret a Homeomorph as a PartialHomeomorph by restricting it to a set s in the domain and to t in the codomain.

Equations

• e.toPartialHomeomorphOfImageEq s t h = { toPartialEquiv := e.toPartialEquivOfImageEq s t h, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

theorem Homeomorph.toPartialHomeomorphOfImageEq_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (t : Set Y) (h : ⇑e '' s = t) : ↑(e.toPartialHomeomorphOfImageEq s t h).symm = ⇑e.symm

@[simp]

theorem Homeomorph.toPartialHomeomorphOfImageEq_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (t : Set Y) (h : ⇑e '' s = t) : ↑(e.toPartialHomeomorphOfImageEq s t h) = ⇑e

@[simp]

theorem Homeomorph.toPartialHomeomorphOfImageEq_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (t : Set Y) (h : ⇑e '' s = t) : (e.toPartialHomeomorphOfImageEq s t h).toPartialEquiv = e.toPartialEquivOfImageEq s t h

theorem Homeomorph.toPartialHomeomorphOfImageEq_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (t : Set Y) (h : ⇑e '' s = t) : (e.toPartialHomeomorphOfImageEq s t h).target = t

theorem Homeomorph.toPartialHomeomorphOfImageEq_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X) (t : Set Y) (h : ⇑e '' s = t) : (e.toPartialHomeomorphOfImageEq s t h).source = s

def Homeomorph.toPartialHomeomorph {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : PartialHomeomorph X Y

A homeomorphism induces a partial homeomorphism on the whole space

Equations

• e.toPartialHomeomorph = e.toPartialHomeomorphOfImageEq Set.univ Set.univ ⋯

@[simp]

theorem Homeomorph.toPartialHomeomorph_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : ↑e.toPartialHomeomorph.symm = ⇑e.symm

@[simp]

theorem Homeomorph.toPartialHomeomorph_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : e.toPartialHomeomorph.target = Set.univ

@[simp]

theorem Homeomorph.toPartialHomeomorph_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : e.toPartialHomeomorph.source = Set.univ

@[simp]

theorem Homeomorph.toPartialHomeomorph_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : ↑e.toPartialHomeomorph = ⇑e

def PartialHomeomorph.replacePartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (e' : PartialEquiv X Y) (h : e.toPartialEquiv = e') : PartialHomeomorph X Y

Replace toPartialEquiv field to provide better definitional equalities.

Equations

• e.replacePartialEquiv e' h = { toPartialEquiv := e', continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

theorem PartialHomeomorph.replacePartialEquiv_eq_self {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (e' : PartialEquiv X Y) (h : e.toPartialEquiv = e') : e.replacePartialEquiv e' h = e

theorem PartialHomeomorph.ext {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : PartialHomeomorph X Y) (h : ∀ (x : X), ↑e x = ↑e' x) (hinv : ∀ (x : Y), ↑e.symm x = ↑e'.symm x) (hs : e.source = e'.source) : e = e'

Two partial homeomorphisms are equal when they have equal toFun, invFun and source. It is not sufficient to have equal toFun and source, as this only determines invFun on the target. This would only be true for a weaker notion of equality, arguably the right one, called EqOnSource.

theorem PartialHomeomorph.ext_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : PartialHomeomorph X Y} : e = e' ↔ (∀ (x : X), ↑e x = ↑e' x) ∧ (∀ (x : Y), ↑e.symm x = ↑e'.symm x) ∧ e.source = e'.source

@[simp]

theorem PartialHomeomorph.symm_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : e.symm.toPartialEquiv = e.symm

theorem PartialHomeomorph.symm_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : e.symm.source = e.target

theorem PartialHomeomorph.symm_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : e.symm.target = e.source

@[simp]

theorem PartialHomeomorph.symm_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : e.symm.symm = e

theorem PartialHomeomorph.symm_bijective {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : Function.Bijective PartialHomeomorph.symm