Partial homeomorphisms: definitions

This file defines homeomorphisms between open subsets of topological spaces. An element e of OpenPartialHomeomorph 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 these sets are open, and that the functions are continuous on them. Equivalently, they are homeomorphisms there.

As in 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.toOpenPartialHomeomorph: associating an open partial homeomorphism to a homeomorphism, with source = target = Set.univ;
• OpenPartialHomeomorph.symm: the inverse of an open partial homeomorphism

Implementation notes

Most statements are copied from their PartialEquiv versions, although some care is required especially when restricting to subsets, as these should be open subsets.

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 OpenPartialHomeomorph (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 open 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
• open_source : IsOpen self.source
• open_target : IsOpen self.target
• continuousOn_toFun : ContinuousOn (↑self.toPartialEquiv) self.source
• continuousOn_invFun : ContinuousOn self.invFun self.target

@[deprecated OpenPartialHomeomorph (since := "2025-08-29")]

def PartialHomeomorph (X : Type u_7) (Y : Type u_8) [TopologicalSpace X] [TopologicalSpace Y] : Type (max u_7 u_8)

Alias of OpenPartialHomeomorph.

---

Partial homeomorphisms, defined on open subsets of the space

Equations

• PartialHomeomorph = OpenPartialHomeomorph

Basic properties; inverse (symm instance)

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

Coercion of an open 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. While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs.

Equations

• ↑e = ↑e.toPartialEquiv

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

Coercion of an OpenPartialHomeomorph to function. Note that an OpenPartialHomeomorph is not DFunLike.

Equations

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

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

The inverse of an open partial homeomorphism

Equations

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

def OpenPartialHomeomorph.Simps.apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph 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

• OpenPartialHomeomorph.Simps.apply e = ↑e

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

See Note [custom simps projection]

Equations

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

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

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

@[simp]

theorem OpenPartialHomeomorph.mk_coe {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (a : IsOpen e.source) (b : IsOpen e.target) (c : ContinuousOn (↑e) e.source) (d : ContinuousOn e.invFun e.target) : ↑{ toPartialEquiv := e, open_source := a, open_target := b, continuousOn_toFun := c, continuousOn_invFun := d } = ↑e

@[simp]

theorem OpenPartialHomeomorph.mk_coe_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialEquiv X Y) (a : IsOpen e.source) (b : IsOpen e.target) (c : ContinuousOn (↑e) e.source) (d : ContinuousOn e.invFun e.target) : ↑{ toPartialEquiv := e, open_source := a, open_target := b, continuousOn_toFun := c, continuousOn_invFun := d }.symm = ↑e.symm

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Variant of map_source, stated for images of subsets of source.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

Equations

• e.toOpenPartialHomeomorphOfImageEq s hs t h = { toPartialEquiv := e.toPartialEquivOfImageEq s t h, open_source := hs, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[deprecated Homeomorph.toOpenPartialHomeomorphOfImageEq (since := "2025-08-29")]

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

Alias of Homeomorph.toOpenPartialHomeomorphOfImageEq.

---

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

Equations

• @Homeomorph.toPartialHomeomorphOfImageEq = @Homeomorph.toOpenPartialHomeomorphOfImageEq

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

A homeomorphism induces an open partial homeomorphism on the whole space

Equations

• e.toOpenPartialHomeomorph = e.toOpenPartialHomeomorphOfImageEq Set.univ ⋯ Set.univ ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[deprecated Homeomorph.toOpenPartialHomeomorph (since := "2025-08-29")]

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

Alias of Homeomorph.toOpenPartialHomeomorph.

---

A homeomorphism induces an open partial homeomorphism on the whole space

Equations

• @Homeomorph.toPartialHomeomorph = @Homeomorph.toOpenPartialHomeomorph

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

Replace toPartialEquiv field to provide better definitional equalities.

Equations

• e.replaceEquiv e' h = { toPartialEquiv := e', open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

theorem OpenPartialHomeomorph.replaceEquiv_eq_self {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (e' : PartialEquiv X Y) (h : e.toPartialEquiv = e') : e.replaceEquiv e' h = e

theorem OpenPartialHomeomorph.ext {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph 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 open 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 OpenPartialHomeomorph.ext_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} : e = e' ↔ (∀ (x : X), ↑e x = ↑e' x) ∧ (∀ (x : Y), ↑e.symm x = ↑e'.symm x) ∧ e.source = e'.source

@[simp]

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

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

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

@[simp]

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

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