Partial homeomorphisms

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

• Homeomorph.toOpenPartialHomeomorph: associating an open partial homeomorphism to a homeomorphism, with source = target = Set.univ;
• OpenPartialHomeomorph.symm: the inverse of an open partial homeomorphism
• OpenPartialHomeomorph.trans: the composition of two open partial homeomorphisms
• OpenPartialHomeomorph.refl: the identity open partial homeomorphism
• OpenPartialHomeomorph.const: an open partial homeomorphism which is a constant map, whose source and target are necessarily singleton sets
• OpenPartialHomeomorph.ofSet: the identity on a set s
• OpenPartialHomeomorph.restr s: restrict an open partial homeomorphism e to e.source ∩ interior s
• OpenPartialHomeomorph.EqOnSource: equivalence relation describing the "right" notion of equality for open partial homeomorphisms
• OpenPartialHomeomorph.prod: the product of two open partial homeomorphisms, as an open partial homeomorphism on the product space
• OpenPartialHomeomorph.pi: the product of a finite family of open partial homeomorphisms
• OpenPartialHomeomorph.disjointUnion: combine two open partial homeomorphisms with disjoint sources and disjoint targets
• OpenPartialHomeomorph.lift_openEmbedding: extend an open partial homeomorphism X → Y under an open embedding X → X', to an open partial homeomorphism X' → Z. (This is used to define the disjoint union of charted spaces.)

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

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

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

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

@[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_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 = _root_.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 = _root_.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.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.eventually_left_inverse {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (y : X) in nhds x, ↑e.symm (↑e y) = y

theorem OpenPartialHomeomorph.eventually_left_inverse' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) : ∀ᶠ (y : X) in nhds (↑e.symm x), ↑e.symm (↑e y) = y

theorem OpenPartialHomeomorph.eventually_right_inverse {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) : ∀ᶠ (y : Y) in nhds x, ↑e (↑e.symm y) = y

theorem OpenPartialHomeomorph.eventually_right_inverse' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (y : Y) in nhds (↑e x), ↑e (↑e.symm y) = y

theorem OpenPartialHomeomorph.eventually_ne_nhdsWithin {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : ∀ᶠ (x' : X) in nhdsWithin x {x}ᶜ, ↑e x' ≠ ↑e x

theorem OpenPartialHomeomorph.nhdsWithin_source_inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) (s : Set X) : nhdsWithin x (e.source ∩ s) = nhdsWithin x s

theorem OpenPartialHomeomorph.nhdsWithin_target_inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : Y} (hx : x ∈ e.target) (s : Set Y) : nhdsWithin x (e.target ∩ s) = nhdsWithin x s

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

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

An open partial homeomorphism is continuous at any point of its source

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

An open partial homeomorphism inverse is continuous at any point of its target

theorem OpenPartialHomeomorph.tendsto_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : Filter.Tendsto (↑e.symm) (nhds (↑e x)) (nhds x)

theorem OpenPartialHomeomorph.map_nhds_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : Filter.map (↑e) (nhds x) = nhds (↑e x)

theorem OpenPartialHomeomorph.symm_map_nhds_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : Filter.map (↑e.symm) (nhds (↑e x)) = nhds x

theorem OpenPartialHomeomorph.image_mem_nhds {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) {s : Set X} (hs : s ∈ nhds x) : ↑e '' s ∈ nhds (↑e x)

theorem OpenPartialHomeomorph.map_nhdsWithin_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) (s : Set X) : Filter.map (↑e) (nhdsWithin x s) = nhdsWithin (↑e x) (↑e '' (e.source ∩ s))

theorem OpenPartialHomeomorph.map_nhdsWithin_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) (s : Set Y) : Filter.map (↑e) (nhdsWithin x (↑e ⁻¹' s)) = nhdsWithin (↑e x) s

theorem OpenPartialHomeomorph.eventually_nhds {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : Y → Prop) (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhds (↑e x), p y) ↔ ∀ᶠ (x : X) in nhds x, p (↑e x)

theorem OpenPartialHomeomorph.eventually_nhds' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : X → Prop) (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhds (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhds x, p x

theorem OpenPartialHomeomorph.eventually_nhdsWithin {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : Y → Prop) {s : Set X} (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhdsWithin (↑e x) (↑e.symm ⁻¹' s), p y) ↔ ∀ᶠ (x : X) in nhdsWithin x s, p (↑e x)

theorem OpenPartialHomeomorph.eventually_nhdsWithin' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {x : X} (p : X → Prop) {s : Set X} (hx : x ∈ e.source) : (∀ᶠ (y : Y) in nhdsWithin (↑e x) (↑e.symm ⁻¹' s), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhdsWithin x s, p x

theorem OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Z} {x : X} {f : X → Z} (hf : ContinuousWithinAt f s x) (hxe : x ∈ e.source) (ht : t ∈ nhds (f x)) : ↑e.symm ⁻¹' s =ᶠ[nhds (↑e x)] e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' t)

This lemma is useful in the manifold library in the case that e is a chart. It states that locally around e x the set e.symm ⁻¹' s is the same as the set intersected with the target of e and some other neighborhood of f x (which will be the source of a chart on Z).

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

OpenPartialHomeomorph.IsImage relation

We say that t : Set Y is an image of s : Set X under an open partial homeomorphism e if any of the following equivalent conditions hold:

• e '' (e.source ∩ s) = e.target ∩ t;
• e.source ∩ e ⁻¹ t = e.source ∩ s;
• ∀ x ∈ e.source, e x ∈ t ↔ x ∈ s (this one is used in the definition).

This definition is a restatement of PartialEquiv.IsImage for open partial homeomorphisms. In this section we transfer API about PartialEquiv.IsImage to open partial homeomorphisms and add a few OpenPartialHomeomorph-specific lemmas like OpenPartialHomeomorph.IsImage.closure.

def OpenPartialHomeomorph.IsImage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) : Prop

We say that t : Set Y is an image of s : Set X under an open partial homeomorphism e if any of the following equivalent conditions hold:

• e '' (e.source ∩ s) = e.target ∩ t;
• e.source ∩ e ⁻¹ t = e.source ∩ s;
• ∀ x ∈ e.source, e x ∈ t ↔ x ∈ s (this one is used in the definition).

Equations

• e.IsImage s t = ∀ ⦃x : X⦄, x ∈ e.source → (↑e x ∈ t ↔ x ∈ s)

theorem OpenPartialHomeomorph.IsImage.toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.IsImage s t

theorem OpenPartialHomeomorph.IsImage.apply_mem_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {x : X} (h : e.IsImage s t) (hx : x ∈ e.source) : ↑e x ∈ t ↔ x ∈ s

theorem OpenPartialHomeomorph.IsImage.symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.symm.IsImage t s

theorem OpenPartialHomeomorph.IsImage.symm_apply_mem_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {y : Y} (h : e.IsImage s t) (hy : y ∈ e.target) : ↑e.symm y ∈ s ↔ y ∈ t

@[simp]

theorem OpenPartialHomeomorph.IsImage.symm_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.symm.IsImage t s ↔ e.IsImage s t

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

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

theorem OpenPartialHomeomorph.IsImage.image_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : ↑e '' (e.source ∩ s) = e.target ∩ t

theorem OpenPartialHomeomorph.IsImage.symm_image_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : ↑e.symm '' (e.target ∩ t) = e.source ∩ s

theorem OpenPartialHomeomorph.IsImage.iff_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s

theorem OpenPartialHomeomorph.IsImage.preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t → e.source ∩ ↑e ⁻¹' t = e.source ∩ s

Alias of the forward direction of OpenPartialHomeomorph.IsImage.iff_preimage_eq.

theorem OpenPartialHomeomorph.IsImage.of_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.source ∩ ↑e ⁻¹' t = e.source ∩ s → e.IsImage s t

Alias of the reverse direction of OpenPartialHomeomorph.IsImage.iff_preimage_eq.

theorem OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t

theorem OpenPartialHomeomorph.IsImage.of_symm_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t → e.IsImage s t

Alias of the reverse direction of OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq.

theorem OpenPartialHomeomorph.IsImage.symm_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t

Alias of the forward direction of OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq.

theorem OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t

theorem OpenPartialHomeomorph.IsImage.symm_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t → e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t

Alias of the forward direction of OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq'.

theorem OpenPartialHomeomorph.IsImage.of_symm_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t → e.IsImage s t

Alias of the reverse direction of OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq'.

theorem OpenPartialHomeomorph.IsImage.iff_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s

theorem OpenPartialHomeomorph.IsImage.preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.IsImage s t → e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s

Alias of the forward direction of OpenPartialHomeomorph.IsImage.iff_preimage_eq'.

theorem OpenPartialHomeomorph.IsImage.of_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.source ∩ ↑e ⁻¹' (e.target ∩ t) = e.source ∩ s → e.IsImage s t

Alias of the reverse direction of OpenPartialHomeomorph.IsImage.iff_preimage_eq'.

theorem OpenPartialHomeomorph.IsImage.of_image_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : ↑e '' (e.source ∩ s) = e.target ∩ t) : e.IsImage s t

theorem OpenPartialHomeomorph.IsImage.of_symm_image_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : ↑e.symm '' (e.target ∩ t) = e.source ∩ s) : e.IsImage s t

theorem OpenPartialHomeomorph.IsImage.compl {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.IsImage sᶜ tᶜ

theorem OpenPartialHomeomorph.IsImage.inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {s' : Set X} {t' : Set Y} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s ∩ s') (t ∩ t')

theorem OpenPartialHomeomorph.IsImage.union {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {s' : Set X} {t' : Set Y} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s ∪ s') (t ∪ t')

theorem OpenPartialHomeomorph.IsImage.diff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {s' : Set X} {t' : Set Y} (h : e.IsImage s t) (h' : e.IsImage s' t') : e.IsImage (s \ s') (t \ t')

theorem OpenPartialHomeomorph.IsImage.leftInvOn_piecewise {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y} [(i : X) → Decidable (i ∈ s)] [(i : Y) → Decidable (i ∈ t)] (h : e.IsImage s t) (h' : e'.IsImage s t) : Set.LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)

theorem OpenPartialHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y} (h : e.IsImage s t) (h' : e'.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)) : e.target ∩ t = e'.target ∩ t

theorem OpenPartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : OpenPartialHomeomorph X Y} (h : e.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)) : Set.EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)

theorem OpenPartialHomeomorph.IsImage.map_nhdsWithin_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {x : X} (h : e.IsImage s t) (hx : x ∈ e.source) : Filter.map (↑e) (nhdsWithin x s) = nhdsWithin (↑e x) t

theorem OpenPartialHomeomorph.IsImage.closure {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.IsImage (closure s) (closure t)

theorem OpenPartialHomeomorph.IsImage.interior {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.IsImage (interior s) (interior t)

theorem OpenPartialHomeomorph.IsImage.frontier {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.IsImage (frontier s) (frontier t)

theorem OpenPartialHomeomorph.IsImage.isOpen_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : IsOpen (e.source ∩ s) ↔ IsOpen (e.target ∩ t)

def OpenPartialHomeomorph.IsImage.restr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) : OpenPartialHomeomorph X Y

Restrict an OpenPartialHomeomorph to a pair of corresponding open sets.

Equations

• h.restr hs = { toPartialEquiv := ⋯.restr, open_source := hs, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.IsImage.restr_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) : (h.restr hs).toPartialEquiv = ⋯.restr

theorem OpenPartialHomeomorph.isImage_source_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.IsImage e.source e.target

theorem OpenPartialHomeomorph.isImage_source_target_of_disjoint {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) (hs : Disjoint e.source e'.source) (ht : Disjoint e.target e'.target) : e.IsImage e'.source e'.target

theorem OpenPartialHomeomorph.preimage_interior {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) : e.source ∩ ↑e ⁻¹' interior s = e.source ∩ interior (↑e ⁻¹' s)

Preimage of interior or interior of preimage coincide for open partial homeomorphisms, when restricted to the source.

theorem OpenPartialHomeomorph.preimage_closure {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) : e.source ∩ ↑e ⁻¹' closure s = e.source ∩ closure (↑e ⁻¹' s)

theorem OpenPartialHomeomorph.preimage_frontier {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set Y) : e.source ∩ ↑e ⁻¹' frontier s = e.source ∩ frontier (↑e ⁻¹' 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.restrict ↑e)) (hs : IsOpen e.source) : OpenPartialHomeomorph X Y

A PartialEquiv with continuous open forward map and open source is a OpenPartialHomeomorph.

Equations

• OpenPartialHomeomorph.ofContinuousOpenRestrict e hc ho hs = { toPartialEquiv := e, open_source := hs, open_target := ⋯, continuousOn_toFun := hc, continuousOn_invFun := ⋯ }

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 with continuous open forward map and open source is a OpenPartialHomeomorph.

Equations

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

def OpenPartialHomeomorph.restrOpen {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) : OpenPartialHomeomorph X Y

Restricting an open partial homeomorphism e to e.source ∩ s when s is open. This is sometimes hard to use because of the openness assumption, but it has the advantage that when it can be used then its PartialEquiv is defeq to PartialEquiv.restr.

Equations

• e.restrOpen s hs = ⋯.restr ⋯

@[simp]

theorem OpenPartialHomeomorph.restrOpen_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) : (e.restrOpen s hs).toPartialEquiv = e.restr s

theorem OpenPartialHomeomorph.restrOpen_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) : (e.restrOpen s hs).source = e.source ∩ s

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

Restricting an open partial homeomorphism e to e.source ∩ interior s. We use the interior to make sure that the restriction is well defined whatever the set s, since open partial homeomorphisms are by definition defined on open sets. In applications where s is open, this coincides with the restriction of partial equivalences.

Equations

• e.restr s = e.restrOpen (interior s) ⋯

@[simp]

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

@[simp]

theorem OpenPartialHomeomorph.restr_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : ↑(e.restr s) = ↑e

theorem OpenPartialHomeomorph.restr_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : (e.restr s).source = e.source ∩ interior s

theorem OpenPartialHomeomorph.restr_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : (e.restr s).target = e.target ∩ ↑e.symm ⁻¹' interior s

@[simp]

theorem OpenPartialHomeomorph.restr_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : (e.restr s).toPartialEquiv = e.restr (interior s)

theorem OpenPartialHomeomorph.restr_source' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) : (e.restr s).source = e.source ∩ s

theorem OpenPartialHomeomorph.restr_toPartialEquiv' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) : (e.restr s).toPartialEquiv = e.restr s

theorem OpenPartialHomeomorph.restr_eq_of_source_subset {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} {s : Set X} (h : e.source ⊆ s) : e.restr s = e

@[simp]

theorem OpenPartialHomeomorph.restr_univ {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : OpenPartialHomeomorph X Y} : e.restr Set.univ = e

theorem OpenPartialHomeomorph.restr_source_inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) (s : Set X) : e.restr (e.source ∩ s) = e.restr s

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

@[simp]

theorem OpenPartialHomeomorph.refl_apply (X : Type u_7) [TopologicalSpace X] : ↑(OpenPartialHomeomorph.refl X) = id

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

theorem OpenPartialHomeomorph.refl_target (X : Type u_7) [TopologicalSpace X] : (OpenPartialHomeomorph.refl X).target = 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

const: PartialEquiv.const as an open partial homeomorphism

def OpenPartialHomeomorph.const {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {a : X} {b : Y} (ha : IsOpen {a}) (hb : IsOpen {b}) : OpenPartialHomeomorph X Y

This is PartialEquiv.single as an open partial homeomorphism: a constant map, whose source and target are necessarily singleton sets.

Equations

• OpenPartialHomeomorph.const ha hb = { toPartialEquiv := PartialEquiv.single a b, open_source := ha, open_target := hb, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.const_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {a : X} {b : Y} (ha : IsOpen {a}) (hb : IsOpen {b}) (x : X) : ↑(const ha hb) x = b

@[simp]

theorem OpenPartialHomeomorph.const_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {a : X} {b : Y} (ha : IsOpen {a}) (hb : IsOpen {b}) : (const ha hb).source = {a}

@[simp]

theorem OpenPartialHomeomorph.const_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {a : X} {b : Y} (ha : IsOpen {a}) (hb : IsOpen {b}) : (const ha hb).target = {b}

ofSet: the identity on a set s

def OpenPartialHomeomorph.ofSet {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) : OpenPartialHomeomorph X X

The identity partial equivalence on a set s

Equations

• OpenPartialHomeomorph.ofSet s hs = { toPartialEquiv := PartialEquiv.ofSet s, open_source := hs, open_target := hs, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.ofSet_apply {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) : ↑(ofSet s hs) = id

theorem OpenPartialHomeomorph.ofSet_source {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) : (ofSet s hs).source = s

theorem OpenPartialHomeomorph.ofSet_target {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) : (ofSet s hs).target = s

@[simp]

theorem OpenPartialHomeomorph.ofSet_toPartialEquiv {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : (ofSet s hs).toPartialEquiv = PartialEquiv.ofSet s

@[simp]

theorem OpenPartialHomeomorph.ofSet_symm {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) : (ofSet s hs).symm = ofSet s hs

@[simp]

theorem OpenPartialHomeomorph.ofSet_univ_eq_refl {X : Type u_1} [TopologicalSpace X] : ofSet Set.univ ⋯ = OpenPartialHomeomorph.refl X

trans: composition of two open partial homeomorphisms

def OpenPartialHomeomorph.trans' {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (h : e.target = e'.source) : OpenPartialHomeomorph X Z

Composition of two open partial homeomorphisms when the target of the first and the source of the second coincide.

Equations

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

@[simp]

theorem OpenPartialHomeomorph.trans'_apply {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (h : e.target = e'.source) (a✝ : X) : ↑(e.trans' e' h) a✝ = ↑e' (↑e a✝)

@[simp]

theorem OpenPartialHomeomorph.trans'_symm_apply {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (h : e.target = e'.source) (a✝ : Z) : ↑(e.trans' e' h).symm a✝ = ↑e.symm (↑e'.symm a✝)

@[simp]

theorem OpenPartialHomeomorph.trans'_toPartialEquiv {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (h : e.target = e'.source) : (e.trans' e' h).toPartialEquiv = e.trans' e'.toPartialEquiv h

theorem OpenPartialHomeomorph.trans'_target {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (h : e.target = e'.source) : (e.trans' e' h).target = e'.target

theorem OpenPartialHomeomorph.trans'_source {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (h : e.target = e'.source) : (e.trans' e' h).source = e.source

def OpenPartialHomeomorph.trans {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : OpenPartialHomeomorph X Z

Composing two open partial homeomorphisms, by restricting to the maximal domain where their composition is well defined. Within the Manifold namespace, there is the notation e ≫ₕ f for this.

Equations

• e.trans e' = (e.symm.restrOpen e'.source ⋯).symm.trans' (e'.restrOpen e.target ⋯) ⋯

@[simp]

theorem OpenPartialHomeomorph.trans_toPartialEquiv {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').toPartialEquiv = e.trans e'.toPartialEquiv

@[simp]

theorem OpenPartialHomeomorph.coe_trans {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : ↑(e.trans e') = ↑e' ∘ ↑e

@[simp]

theorem OpenPartialHomeomorph.coe_trans_symm {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : ↑(e.trans e').symm = ↑e.symm ∘ ↑e'.symm

theorem OpenPartialHomeomorph.trans_apply {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) {x : X} : ↑(e.trans e') x = ↑e' (↑e x)

theorem OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').symm = e'.symm.trans e.symm

theorem OpenPartialHomeomorph.trans_source {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').source = e.source ∩ ↑e ⁻¹' e'.source

theorem OpenPartialHomeomorph.trans_source' {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)

theorem OpenPartialHomeomorph.trans_source'' {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)

theorem OpenPartialHomeomorph.image_trans_source {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : ↑e '' (e.trans e').source = e.target ∩ e'.source

theorem OpenPartialHomeomorph.trans_target {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' e.target

theorem OpenPartialHomeomorph.trans_target' {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' (e'.source ∩ e.target)

theorem OpenPartialHomeomorph.trans_target'' {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : (e.trans e').target = ↑e' '' (e'.source ∩ e.target)

theorem OpenPartialHomeomorph.inv_image_trans_target {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) : ↑e'.symm '' (e.trans e').target = e'.source ∩ e.target

theorem OpenPartialHomeomorph.trans_assoc {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (e'' : OpenPartialHomeomorph Z Z') : (e.trans e').trans e'' = e.trans (e'.trans e'')

@[simp]

theorem OpenPartialHomeomorph.trans_refl {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.trans (OpenPartialHomeomorph.refl Y) = e

@[simp]

theorem OpenPartialHomeomorph.refl_trans {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : (OpenPartialHomeomorph.refl X).trans e = e

theorem OpenPartialHomeomorph.trans_ofSet {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set Y} (hs : IsOpen s) : e.trans (ofSet s hs) = e.restr (↑e ⁻¹' s)

theorem OpenPartialHomeomorph.trans_of_set' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set Y} (hs : IsOpen s) : e.trans (ofSet s hs) = e.restr (e.source ∩ ↑e ⁻¹' s)

theorem OpenPartialHomeomorph.ofSet_trans {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) : (ofSet s hs).trans e = e.restr s

theorem OpenPartialHomeomorph.ofSet_trans' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) : (ofSet s hs).trans e = e.restr (e.source ∩ s)

@[simp]

theorem OpenPartialHomeomorph.ofSet_trans_ofSet {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) {s' : Set X} (hs' : IsOpen s') : (ofSet s hs).trans (ofSet s' hs') = ofSet (s ∩ s') ⋯

theorem OpenPartialHomeomorph.restr_trans {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (s : Set X) : (e.restr s).trans e' = (e.trans e').restr s

EqOnSource: equivalence on their source

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

EqOnSource e e' means that e and e' have the same source, and coincide there. They should really be considered the same partial equivalence.

Equations

• e.EqOnSource e' = (e.source = e'.source ∧ Set.EqOn (↑e) (↑e') e.source)

theorem OpenPartialHomeomorph.eqOnSource_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) : e.EqOnSource e' ↔ e.EqOnSource e'.toPartialEquiv

instance OpenPartialHomeomorph.eqOnSourceSetoid {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : Setoid (OpenPartialHomeomorph X Y)

EqOnSource is an equivalence relation.

Equations

• OpenPartialHomeomorph.eqOnSourceSetoid = { r := OpenPartialHomeomorph.EqOnSource, iseqv := ⋯ }

theorem OpenPartialHomeomorph.eqOnSource_refl {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e ≈ e

theorem OpenPartialHomeomorph.EqOnSource.symm' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : e.symm ≈ e'.symm

If two open partial homeomorphisms are equivalent, so are their inverses.

theorem OpenPartialHomeomorph.EqOnSource.source_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : e.source = e'.source

Two equivalent open partial homeomorphisms have the same source.

theorem OpenPartialHomeomorph.EqOnSource.target_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : e.target = e'.target

Two equivalent open partial homeomorphisms have the same target.

theorem OpenPartialHomeomorph.EqOnSource.eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : Set.EqOn (↑e) (↑e') e.source

Two equivalent open partial homeomorphisms have coinciding toFun on the source

theorem OpenPartialHomeomorph.EqOnSource.symm_eqOn_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') : Set.EqOn (↑e.symm) (↑e'.symm) e.target

Two equivalent open partial homeomorphisms have coinciding invFun on the target

theorem OpenPartialHomeomorph.EqOnSource.trans' {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {e e' : OpenPartialHomeomorph X Y} {f f' : OpenPartialHomeomorph Y Z} (he : e ≈ e') (hf : f ≈ f') : e.trans f ≈ e'.trans f'

Composition of open partial homeomorphisms respects equivalence.

theorem OpenPartialHomeomorph.EqOnSource.restr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (he : e ≈ e') (s : Set X) : e.restr s ≈ e'.restr s

Restriction of open partial homeomorphisms respects equivalence

theorem OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : Set.EqOn (↑e) (↑e') (e.source ∩ e'.source)) : e.restr e'.source ≈ e'.restr e.source

Two equivalent open partial homeomorphisms are equal when the source and target are univ.

theorem OpenPartialHomeomorph.self_trans_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.trans e.symm ≈ ofSet e.source ⋯

Composition of an open partial homeomorphism and its inverse is equivalent to the restriction of the identity to the source

theorem OpenPartialHomeomorph.symm_trans_self {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) : e.symm.trans e ≈ ofSet e.target ⋯

theorem OpenPartialHomeomorph.eq_of_eqOnSource_univ {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') (s : e.source = Set.univ) (t : e.target = Set.univ) : e = e'

theorem OpenPartialHomeomorph.restr_symm_trans {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} {e' : OpenPartialHomeomorph X Y} (hs : IsOpen s) (hs' : IsOpen (↑e '' s)) (hs'' : s ⊆ e.source) : (e.restr s).symm.trans e' ≈ (e.symm.trans e').restr (↑e '' s)

theorem OpenPartialHomeomorph.symm_trans_restr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} (e' : OpenPartialHomeomorph X Y) (hs : IsOpen s) : e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ ↑e'.symm ⁻¹' s)

theorem OpenPartialHomeomorph.restr_eqOnSource_restr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s s' : Set X} (hss' : e.source ∩ interior s = e.source ∩ interior s') : e.restr s ≈ e.restr s'

theorem OpenPartialHomeomorph.restr_inter_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : Set X} : e.restr (e.source ∩ s) ≈ e.restr s

product of two open partial homeomorphisms

def OpenPartialHomeomorph.prod {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') : OpenPartialHomeomorph (X × Y) (X' × Y')

The product of two open partial homeomorphisms, as an open partial homeomorphism on the product space.

Equations

• eX.prod eY = { toPartialEquiv := eX.prod eY.toPartialEquiv, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.prod_toPartialEquiv {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') : (eX.prod eY).toPartialEquiv = eX.prod eY.toPartialEquiv

@[simp]

theorem OpenPartialHomeomorph.prod_apply {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') : ↑(eX.prod eY) = fun (p : X × Y) => (↑eX p.1, ↑eY p.2)

theorem OpenPartialHomeomorph.prod_source {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') : (eX.prod eY).source = eX.source ×ˢ eY.source

theorem OpenPartialHomeomorph.prod_target {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') : (eX.prod eY).target = eX.target ×ˢ eY.target

theorem OpenPartialHomeomorph.prod_symm_apply {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') (p : X' × Y') : ↑(eX.prod eY).symm p = (↑eX.symm p.1, ↑eY.symm p.2)

@[simp]

theorem OpenPartialHomeomorph.prod_symm {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') : (eX.prod eY).symm = eX.symm.prod eY.symm

@[simp]

theorem OpenPartialHomeomorph.refl_prod_refl {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : (OpenPartialHomeomorph.refl X).prod (OpenPartialHomeomorph.refl Y) = OpenPartialHomeomorph.refl (X × Y)

@[simp]

theorem OpenPartialHomeomorph.prod_trans {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} {Z : Type u_5} {Z' : Type u_6} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] [TopologicalSpace Z] [TopologicalSpace Z'] (e : OpenPartialHomeomorph X Y) (f : OpenPartialHomeomorph Y Z) (e' : OpenPartialHomeomorph X' Y') (f' : OpenPartialHomeomorph Y' Z') : (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')

theorem OpenPartialHomeomorph.prod_eq_prod_of_nonempty {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] {eX eX' : OpenPartialHomeomorph X X'} {eY eY' : OpenPartialHomeomorph Y Y'} (h : (eX.prod eY).source.Nonempty) : eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

theorem OpenPartialHomeomorph.prod_eq_prod_of_nonempty' {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] {eX eX' : OpenPartialHomeomorph X X'} {eY eY' : OpenPartialHomeomorph Y Y'} (h : (eX'.prod eY').source.Nonempty) : eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

finite product of partial homeomorphisms

def OpenPartialHomeomorph.pi {ι : Type u_7} [Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)) : OpenPartialHomeomorph ((i : ι) → X i) ((i : ι) → Y i)

The product of a finite family of OpenPartialHomeomorphs.

Equations

• OpenPartialHomeomorph.pi ei = { toPartialEquiv := PartialEquiv.pi fun (i : ι) => (ei i).toPartialEquiv, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.pi_toPartialEquiv {ι : Type u_7} [Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)) : (pi ei).toPartialEquiv = PartialEquiv.pi fun (i : ι) => (ei i).toPartialEquiv

@[simp]

theorem OpenPartialHomeomorph.pi_target {ι : Type u_7} [Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)) : (pi ei).target = Set.univ.pi fun (i : ι) => (ei i).target

@[simp]

theorem OpenPartialHomeomorph.pi_symm_apply {ι : Type u_7} [Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)) (a✝ : (i : ι) → Y i) (i : ι) : ↑(pi ei).symm a✝ i = ↑(ei i).symm (a✝ i)

@[simp]

theorem OpenPartialHomeomorph.pi_source {ι : Type u_7} [Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)) : (pi ei).source = Set.univ.pi fun (i : ι) => (ei i).source

@[simp]

theorem OpenPartialHomeomorph.pi_apply {ι : Type u_7} [Finite ι] {X : ι → Type u_8} {Y : ι → Type u_9} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] (ei : (i : ι) → OpenPartialHomeomorph (X i) (Y i)) (a✝ : (i : ι) → X i) (i : ι) : ↑(pi ei) a✝ i = ↑(ei i) (a✝ i)

combining two partial homeomorphisms using Set.piecewise

def OpenPartialHomeomorph.piecewise {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [(x : X) → Decidable (x ∈ s)] [(y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : OpenPartialHomeomorph X Y

Combine two OpenPartialHomeomorphs using Set.piecewise. The source of the new OpenPartialHomeomorph is s.ite e.source e'.source = e.source ∩ s ∪ e'.source \ s, and similarly for target. The function sends e.source ∩ s to e.target ∩ t using e and e'.source \ s to e'.target \ t using e', and similarly for the inverse function. To ensure the maps toFun and invFun are inverse of each other on the new source and target, the definition assumes that the sets s and t are related both by e.is_image and e'.is_image. To ensure that the new maps are continuous on source/target, it also assumes that e.source and e'.source meet frontier s on the same set and e x = e' x on this intersection.

Equations

• e.piecewise e' s t H H' Hs Heq = { toPartialEquiv := e.piecewise e'.toPartialEquiv s t H H', open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.piecewise_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [(x : X) → Decidable (x ∈ s)] [(y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : ↑(e.piecewise e' s t H H' Hs Heq) = s.piecewise ↑e ↑e'

@[simp]

theorem OpenPartialHomeomorph.piecewise_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [(x : X) → Decidable (x ∈ s)] [(y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : (e.piecewise e' s t H H' Hs Heq).toPartialEquiv = e.piecewise e'.toPartialEquiv s t H H'

@[simp]

theorem OpenPartialHomeomorph.symm_piecewise {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) {s : Set X} {t : Set Y} [(x : X) → Decidable (x ∈ s)] [(y : Y) → Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t) (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)) : (e.piecewise e' s t H H' Hs Heq).symm = e.symm.piecewise e'.symm t s ⋯ ⋯ ⋯ ⋯

def OpenPartialHomeomorph.disjointUnion {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : OpenPartialHomeomorph X Y) [(x : X) → Decidable (x ∈ e.source)] [(y : Y) → Decidable (y ∈ e.target)] (Hs : Disjoint e.source e'.source) (Ht : Disjoint e.target e'.target) : OpenPartialHomeomorph X Y

Combine two OpenPartialHomeomorphs with disjoint sources and disjoint targets. We reuse OpenPartialHomeomorph.piecewise then override toPartialEquiv to PartialEquiv.disjointUnion. This way we have better definitional equalities for source and target.

Equations

• e.disjointUnion e' Hs Ht = (e.piecewise e' e.source e.target ⋯ ⋯ ⋯ ⋯).replaceEquiv (e.disjointUnion e'.toPartialEquiv Hs Ht) ⋯

theorem OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {s : Set Y} {x : Y} (h : x ∈ e.target) : ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e ⁻¹' s) (↑e.symm x)

Continuity within a set at a point can be read under right composition with a local homeomorphism, if the point is in its target

theorem OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {x : Y} (h : x ∈ e.target) : ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)

Continuity at a point can be read under right composition with an open partial homeomorphism, if the point is in its target

theorem OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_right {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Y → Z} {s : Set Y} (h : s ⊆ e.target) : ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s)

A function is continuous on a set if and only if its composition with an open partial homeomorphism on the right is continuous on the corresponding set.

theorem OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} {s : Set Z} {x : Z} (hx : f x ∈ e.source) (h : f ⁻¹' e.source ∈ nhdsWithin x s) : ContinuousWithinAt f s x ↔ ContinuousWithinAt (↑e ∘ f) s x

Continuity within a set at a point can be read under left composition with a local homeomorphism if a neighborhood of the initial point is sent to the source of the local homeomorphism

theorem OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} {x : Z} (h : f ⁻¹' e.source ∈ nhds x) : ContinuousAt f x ↔ ContinuousAt (↑e ∘ f) x

Continuity at a point can be read under left composition with an open partial homeomorphism if a neighborhood of the initial point is sent to the source of the partial homeomorphism

theorem OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_left {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} {s : Set Z} (h : s ⊆ f ⁻¹' e.source) : ContinuousOn f s ↔ ContinuousOn (↑e ∘ f) s

A function is continuous on a set if and only if its composition with an open partial homeomorphism on the left is continuous on the corresponding set.

theorem OpenPartialHomeomorph.continuous_iff_continuous_comp_left {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} (h : f ⁻¹' e.source = Set.univ) : Continuous f ↔ Continuous (↑e ∘ f)

A function is continuous if and only if its composition with an open partial homeomorphism on the left is continuous and its image is contained in the source.

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

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

@[simp]

theorem OpenPartialHomeomorph.homeomorphOfImageSubsetSource_symm_apply {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✝ = Set.MapsTo.restrict (↑e.symm) t s ⋯ a✝

@[simp]

theorem OpenPartialHomeomorph.homeomorphOfImageSubsetSource_apply {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✝ = Set.MapsTo.restrict (↑e) s t ⋯ 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 ⋯ ⋯

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

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

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) : X ≃ₜ Y

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' = { toFun := ↑e, invFun := ↑e.symm, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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

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

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.

@[simp]

theorem Homeomorph.refl_toOpenPartialHomeomorph {X : Type u_1} [TopologicalSpace X] : (Homeomorph.refl X).toOpenPartialHomeomorph = OpenPartialHomeomorph.refl X

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

theorem Homeomorph.refl_toPartialHomeomorph {X : Type u_1} [TopologicalSpace X] : (Homeomorph.refl X).toOpenPartialHomeomorph = OpenPartialHomeomorph.refl X

Alias of Homeomorph.refl_toOpenPartialHomeomorph.

@[simp]

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

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

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

Alias of Homeomorph.symm_toOpenPartialHomeomorph.

@[simp]

theorem Homeomorph.trans_toOpenPartialHomeomorph {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (e' : Y ≃ₜ Z) : (e.trans e').toOpenPartialHomeomorph = e.toOpenPartialHomeomorph.trans e'.toOpenPartialHomeomorph

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

theorem Homeomorph.trans_toPartialHomeomorph {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (e' : Y ≃ₜ Z) : (e.trans e').toOpenPartialHomeomorph = e.toOpenPartialHomeomorph.trans e'.toOpenPartialHomeomorph

Alias of Homeomorph.trans_toOpenPartialHomeomorph.

def Homeomorph.transOpenPartialHomeomorph {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : OpenPartialHomeomorph X Z

Precompose an open partial homeomorphism with a homeomorphism. We modify the source and target to have better definitional behavior.

Equations

• e.transOpenPartialHomeomorph f' = { toPartialEquiv := e.transPartialEquiv f'.toPartialEquiv, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

theorem Homeomorph.transOpenPartialHomeomorph_source {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : (e.transOpenPartialHomeomorph f').source = ⇑e ⁻¹' f'.source

@[simp]

theorem Homeomorph.transOpenPartialHomeomorph_target {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : (e.transOpenPartialHomeomorph f').target = f'.target

@[simp]

theorem Homeomorph.transOpenPartialHomeomorph_apply {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : ↑(e.transOpenPartialHomeomorph f') = ↑f' ∘ ⇑e

@[simp]

theorem Homeomorph.transOpenPartialHomeomorph_symm_apply {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : ↑(e.transOpenPartialHomeomorph f').symm = ⇑e.symm ∘ ↑f'.symm

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

def Homeomorph.transPartialHomeomorph {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : OpenPartialHomeomorph X Z

Alias of Homeomorph.transOpenPartialHomeomorph.

---

Precompose an open partial homeomorphism with a homeomorphism. We modify the source and target to have better definitional behavior.

Equations

• @Homeomorph.transPartialHomeomorph = @Homeomorph.transOpenPartialHomeomorph

theorem Homeomorph.transOpenPartialHomeomorph_eq_trans {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : e.transOpenPartialHomeomorph f' = e.toOpenPartialHomeomorph.trans f'

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

theorem Homeomorph.transPartialHomeomorph_eq_trans {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) : e.transOpenPartialHomeomorph f' = e.toOpenPartialHomeomorph.trans f'

Alias of Homeomorph.transOpenPartialHomeomorph_eq_trans.

@[simp]

theorem Homeomorph.transOpenPartialHomeomorph_trans {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] (e : X ≃ₜ Y) (f : OpenPartialHomeomorph Y Z) (f' : OpenPartialHomeomorph Z Z') : (e.transOpenPartialHomeomorph f).trans f' = e.transOpenPartialHomeomorph (f.trans f')

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

theorem Homeomorph.transPartialHomeomorph_trans {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] (e : X ≃ₜ Y) (f : OpenPartialHomeomorph Y Z) (f' : OpenPartialHomeomorph Z Z') : (e.transOpenPartialHomeomorph f).trans f' = e.transOpenPartialHomeomorph (f.trans f')

Alias of Homeomorph.transOpenPartialHomeomorph_trans.

@[simp]

theorem Homeomorph.trans_transOpenPartialHomeomorph {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] (e : X ≃ₜ Y) (e' : Y ≃ₜ Z) (f'' : OpenPartialHomeomorph Z Z') : (e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'')

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

theorem Homeomorph.trans_transPartialHomeomorph {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] (e : X ≃ₜ Y) (e' : Y ≃ₜ Z) (f'' : OpenPartialHomeomorph Z Z') : (e.trans e').transOpenPartialHomeomorph f'' = e.transOpenPartialHomeomorph (e'.transOpenPartialHomeomorph f'')

Alias of Homeomorph.trans_transOpenPartialHomeomorph.

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

Equations

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

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

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

def Topology.IsOpenEmbedding.toPartialHomeomorph {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] : OpenPartialHomeomorph X Y

Alias of Topology.IsOpenEmbedding.toOpenPartialHomeomorph.

---

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

Equations

• @Topology.IsOpenEmbedding.toPartialHomeomorph = @Topology.IsOpenEmbedding.toOpenPartialHomeomorph

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

@[deprecated Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv (since := "2025-08-29")]

theorem Topology.IsOpenEmbedding.toPartialHomeomorph_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

Alias of Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv.

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

@[deprecated Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv (since := "2025-08-29")]

theorem Topology.IsOpenEmbedding.toPartialHomeomorph_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

Alias of Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv.

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 ⋯

@[deprecated TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe (since := "2025-08-29")]

def TopologicalSpace.Opens.partialHomeomorphSubtypeCoe {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) : OpenPartialHomeomorph (↥s) X

Alias of TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe.

---

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

• @TopologicalSpace.Opens.partialHomeomorphSubtypeCoe = @TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe

@[simp]

theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_coe {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) : ↑(s.openPartialHomeomorphSubtypeCoe hs) = Subtype.val

@[deprecated TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_coe (since := "2025-08-29")]

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

Alias of TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_coe.

@[simp]

theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) : (s.openPartialHomeomorphSubtypeCoe hs).source = Set.univ

@[deprecated TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source (since := "2025-08-29")]

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

Alias of TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source.

@[simp]

theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) : (s.openPartialHomeomorphSubtypeCoe hs).target = ↑s

@[deprecated TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target (since := "2025-08-29")]

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

Alias of TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target.

def OpenPartialHomeomorph.transHomeomorph {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : OpenPartialHomeomorph X Z

Postcompose an open partial homeomorphism with a homeomorphism. We modify the source and target to have better definitional behavior.

Equations

• e.transHomeomorph f' = { toPartialEquiv := e.transEquiv f'.toEquiv, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[simp]

theorem OpenPartialHomeomorph.transHomeomorph_apply {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : ↑(e.transHomeomorph f') = ⇑f' ∘ ↑e

@[simp]

theorem OpenPartialHomeomorph.transHomeomorph_target {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : (e.transHomeomorph f').target = ⇑f'.symm ⁻¹' e.target

@[simp]

theorem OpenPartialHomeomorph.transHomeomorph_symm_apply {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : ↑(e.transHomeomorph f').symm = ↑e.symm ∘ ⇑f'.symm

@[simp]

theorem OpenPartialHomeomorph.transHomeomorph_source {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : (e.transHomeomorph f').source = e.source

theorem OpenPartialHomeomorph.transHomeomorph_eq_trans {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : e.transHomeomorph f' = e.trans f'.toOpenPartialHomeomorph

@[simp]

theorem OpenPartialHomeomorph.transHomeomorph_transHomeomorph {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) (f'' : Z ≃ₜ Z') : (e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'')

@[simp]

theorem OpenPartialHomeomorph.trans_transHomeomorph {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (f'' : Z ≃ₜ Z') : (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')

subtypeRestr: restriction to a subtype

noncomputable def OpenPartialHomeomorph.subtypeRestr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) : OpenPartialHomeomorph (↥s) Y

The restriction of an open partial homeomorphism e to an open subset s of the domain type produces an open partial homeomorphism whose domain is the subtype s.

Equations

• e.subtypeRestr hs = (s.openPartialHomeomorphSubtypeCoe hs).trans e

theorem OpenPartialHomeomorph.subtypeRestr_def {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) : e.subtypeRestr hs = (s.openPartialHomeomorphSubtypeCoe hs).trans e

@[simp]

theorem OpenPartialHomeomorph.subtypeRestr_coe {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) : ↑(e.subtypeRestr hs) = (↑s).restrict ↑e

@[simp]

theorem OpenPartialHomeomorph.subtypeRestr_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) : (e.subtypeRestr hs).source = Subtype.val ⁻¹' e.source

theorem OpenPartialHomeomorph.map_subtype_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) {x : ↥s} (hxe : ↑x ∈ e.source) : ↑e ↑x ∈ (e.subtypeRestr hs).target

theorem OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) (f f' : OpenPartialHomeomorph X Y) : (f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈ (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)

This lemma characterizes the transition functions of an open subset in terms of the transition functions of the original space.

theorem OpenPartialHomeomorph.subtypeRestr_symm_eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {U : TopologicalSpace.Opens X} (hU : Nonempty ↥U) : Set.EqOn (↑e.symm) (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target

theorem OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {U V : TopologicalSpace.Opens X} (hU : Nonempty ↥U) (hV : Nonempty ↥V) (hUV : U ≤ V) : Set.EqOn (↑(e.subtypeRestr hV).symm) (Set.inclusion hUV ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target

noncomputable def OpenPartialHomeomorph.lift_openEmbedding {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : OpenPartialHomeomorph X' Z

Extend an open partial homeomorphism e : X → Z to X' → Z, using an open embedding ι : X → X'. On ι(X), the extension is specified by e; its value elsewhere is arbitrary (and uninteresting).

Equations

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

@[simp]

theorem OpenPartialHomeomorph.lift_openEmbedding_toFun {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : ↑(e.lift_openEmbedding hf) = Function.extend f ↑e fun (x : X') => Classical.arbitrary Z

theorem OpenPartialHomeomorph.lift_openEmbedding_apply {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) {x : X} : ↑(e.lift_openEmbedding hf) (f x) = ↑e x

@[simp]

theorem OpenPartialHomeomorph.lift_openEmbedding_source {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).source = f '' e.source

@[simp]

theorem OpenPartialHomeomorph.lift_openEmbedding_target {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).target = e.target

@[simp]

theorem OpenPartialHomeomorph.lift_openEmbedding_symm {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : ↑(e.lift_openEmbedding hf).symm = f ∘ ↑e.symm

@[simp]

theorem OpenPartialHomeomorph.lift_openEmbedding_symm_source {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).symm.source = e.target

@[simp]

theorem OpenPartialHomeomorph.lift_openEmbedding_symm_target {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).symm.target = f '' e.source

theorem OpenPartialHomeomorph.lift_openEmbedding_trans_apply {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e e' : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) (z : Z) : ↑((e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf)) z = ↑(e.symm.trans e') z

@[simp]

theorem OpenPartialHomeomorph.lift_openEmbedding_trans {X : Type u_7} {X' : Type u_8} {Z : Type u_9} [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Z] [Nonempty Z] {f : X → X'} (e e' : OpenPartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'