Partial homeomorphisms

This file defines homeomorphisms between open subsets of topological spaces. An element e of PartialHomeomorph X Y is an extension of PartialEquiv X Y, i.e., it is a pair of functions e.toFun and e.invFun, inverse of each other on the sets e.source and e.target. Additionally, we require that 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.toPartialHomeomorph: associating a partial homeomorphism to a homeomorphism, with source = target = Set.univ;
• PartialHomeomorph.symm: the inverse of a partial homeomorphism
• PartialHomeomorph.trans: the composition of two partial homeomorphisms
• PartialHomeomorph.refl: the identity partial homeomorphism
• PartialHomeomorph.ofSet: the identity on a set s
• PartialHomeomorph.EqOnSource: equivalence relation describing the "right" notion of equality for partial homeomorphisms

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 PartialHomeomorph (X : Type u_7) (Y : Type u_8) [TopologicalSpace X] [TopologicalSpace Y] extends PartialEquiv X Y : Type (max u_7 u_8)

Partial homeomorphisms, defined on 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

Basic properties; inverse (symm instance)

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

Coercion of a partial homeomorphisms to a function. We don't use e.toFun because it is actually e.toPartialEquiv.toFun, so simp will apply lemmas about toPartialEquiv. 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 PartialHomeomorph.instCoeFunForall {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : CoeFun (PartialHomeomorph X Y) fun (x : PartialHomeomorph X Y) => X → Y

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

Equations

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

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

The inverse of a partial homeomorphism

Equations

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

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

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

Equations

• PartialHomeomorph.Simps.apply e = ↑e

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

See Note [custom simps projection]

Equations

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

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

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

@[simp]

theorem PartialHomeomorph.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 PartialHomeomorph.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 PartialHomeomorph.toPartialEquiv_injective {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] : Function.Injective toPartialEquiv

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

@[simp]

theorem Homeomorph.toPartialHomeomorphOfImageEq_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.toPartialHomeomorphOfImageEq s hs t h) = ⇑e

@[simp]

theorem Homeomorph.toPartialHomeomorphOfImageEq_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.toPartialHomeomorphOfImageEq s hs t h).symm = ⇑e.symm

@[simp]

theorem Homeomorph.toPartialHomeomorphOfImageEq_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.toPartialHomeomorphOfImageEq s hs t h).toPartialEquiv = e.toPartialEquivOfImageEq s t h

theorem Homeomorph.toPartialHomeomorphOfImageEq_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.toPartialHomeomorphOfImageEq s hs t h).source = s

theorem Homeomorph.toPartialHomeomorphOfImageEq_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.toPartialHomeomorphOfImageEq s hs t h).target = t

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

A homeomorphism induces a partial homeomorphism on the whole space

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Replace toPartialEquiv field to provide better definitional equalities.

Equations

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

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

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

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

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

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

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

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

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

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

theorem PartialHomeomorph.image_eq_target_inter_inv_preimage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set X} (h : s ⊆ e.source) : ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s

theorem PartialHomeomorph.image_source_inter_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (s : Set X) : ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s

theorem PartialHomeomorph.image_source_inter_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (s : Set X) : ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)

theorem PartialHomeomorph.symm_image_eq_source_inter_preimage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set Y} (h : s ⊆ e.target) : ↑e.symm '' s = e.source ∩ ↑e ⁻¹' s

theorem PartialHomeomorph.symm_image_target_inter_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (s : Set Y) : ↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' (e.target ∩ s)

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

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

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

A partial homeomorphism is continuous at any point of its source

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

A partial homeomorphism inverse is continuous at any point of its target

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

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

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

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

theorem PartialHomeomorph.map_nhdsWithin_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph 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 PartialHomeomorph.map_nhdsWithin_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) (s : Set Y) : Filter.map (↑e) (nhdsWithin x (↑e ⁻¹' s)) = nhdsWithin (↑e x) s

theorem PartialHomeomorph.eventually_nhds {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph 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 PartialHomeomorph.eventually_nhds' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph 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 PartialHomeomorph.eventually_nhdsWithin {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph 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 PartialHomeomorph.eventually_nhdsWithin' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph 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 PartialHomeomorph.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 : PartialHomeomorph 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 PartialHomeomorph.isOpen_inter_preimage {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set Y} (hs : IsOpen s) : IsOpen (e.source ∩ ↑e ⁻¹' s)

theorem PartialHomeomorph.isOpen_inter_preimage_symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) : IsOpen (e.target ∩ ↑e.symm ⁻¹' s)

theorem PartialHomeomorph.isOpen_image_of_subset_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set X} (hs : IsOpen s) (hse : s ⊆ e.source) : IsOpen (↑e '' s)

A partial homeomorphism is an open map on its source: the image of an open subset of the source is open.

theorem PartialHomeomorph.isOpen_image_source_inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph 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 PartialHomeomorph.isOpen_image_symm_of_subset_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {t : Set Y} (ht : IsOpen t) (hte : t ⊆ e.target) : IsOpen (↑e.symm '' t)

The inverse of a partial homeomorphism e is an open map on e.target.

theorem PartialHomeomorph.isOpen_symm_image_iff_of_subset_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {t : Set Y} (hs : t ⊆ e.target) : IsOpen (↑e.symm '' t) ↔ IsOpen t

theorem PartialHomeomorph.isOpen_image_iff_of_subset_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set X} (hs : s ⊆ e.source) : IsOpen (↑e '' s) ↔ IsOpen s

PartialHomeomorph.IsImage relation

We say that t : Set Y is an image of s : Set X under a 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 partial homeomorphisms. In this section we transfer API about PartialEquiv.IsImage to partial homeomorphisms and add a few PartialHomeomorph-specific lemmas like PartialHomeomorph.IsImage.closure.

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

We say that t : Set Y is an image of s : Set X under a 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 PartialHomeomorph.IsImage.toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.IsImage s t

theorem PartialHomeomorph.IsImage.apply_mem_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.symm {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.symm.IsImage t s

theorem PartialHomeomorph.IsImage.symm_apply_mem_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.symm_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph X Y} {s : Set X} {t : Set Y} : e.symm.IsImage t s ↔ e.IsImage s t

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

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

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

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

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

theorem PartialHomeomorph.IsImage.of_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.iff_preimage_eq.

theorem PartialHomeomorph.IsImage.preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.iff_preimage_eq.

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

theorem PartialHomeomorph.IsImage.of_symm_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.iff_symm_preimage_eq.

theorem PartialHomeomorph.IsImage.symm_preimage_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.iff_symm_preimage_eq.

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

theorem PartialHomeomorph.IsImage.of_symm_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.iff_symm_preimage_eq'.

theorem PartialHomeomorph.IsImage.symm_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.iff_symm_preimage_eq'.

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

theorem PartialHomeomorph.IsImage.of_preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.iff_preimage_eq'.

theorem PartialHomeomorph.IsImage.preimage_eq' {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.iff_preimage_eq'.

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

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

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

theorem PartialHomeomorph.IsImage.inter {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.union {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.diff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.leftInvOn_piecewise {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : PartialHomeomorph 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 PartialHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : PartialHomeomorph 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 PartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph X Y} {s : Set X} {t : Set Y} {e' : PartialHomeomorph 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 PartialHomeomorph.IsImage.map_nhdsWithin_eq {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph 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 PartialHomeomorph.IsImage.closure {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] {e : PartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) : e.IsImage (closure s) (closure t)

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

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

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

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

Restrict a PartialHomeomorph to a pair of corresponding open sets.

Equations

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

@[simp]

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

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

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

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

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

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

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

def PartialHomeomorph.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) : PartialHomeomorph X Y

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

Equations

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

def PartialHomeomorph.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) : PartialHomeomorph X Y

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

Equations

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

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

Restricting a 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 PartialHomeomorph.restrOpen_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (s : Set X) (hs : IsOpen s) : (e.restrOpen s hs).toPartialEquiv = e.restr s

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

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

Restricting a 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 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 PartialHomeomorph.restr_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (s : Set X) : ↑(e.restr s).symm = ↑e.symm

@[simp]

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

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

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

@[simp]

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

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

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

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

@[simp]

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

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

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

The identity on the whole space as a partial homeomorphism.

Equations

• PartialHomeomorph.refl X = (Homeomorph.refl X).toPartialHomeomorph

@[simp]

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

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

theorem PartialHomeomorph.refl_target (X : Type u_7) [TopologicalSpace X] : (PartialHomeomorph.refl X).target = Set.univ

@[simp]

theorem PartialHomeomorph.refl_partialEquiv {X : Type u_1} [TopologicalSpace X] : (PartialHomeomorph.refl X).toPartialEquiv = PartialEquiv.refl X

@[simp]

theorem PartialHomeomorph.refl_symm {X : Type u_1} [TopologicalSpace X] : (PartialHomeomorph.refl X).symm = PartialHomeomorph.refl X

ofSet: the identity on a set s

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

The identity partial equivalence on a set s

Equations

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

trans: composition of two partial homeomorphisms

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

Composition of two 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 PartialHomeomorph.trans'_apply {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph X Y) (e' : PartialHomeomorph Y Z) (h : e.target = e'.source) (a✝ : X) : ↑(e.trans' e' h) a✝ = ↑e' (↑e a✝)

@[simp]

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

@[simp]

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

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

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

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

Composing two 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 PartialHomeomorph.trans_toPartialEquiv {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph X Y) (e' : PartialHomeomorph Y Z) : (e.trans e').toPartialEquiv = e.trans e'.toPartialEquiv

@[simp]

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

@[simp]

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

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

theorem PartialHomeomorph.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 : PartialHomeomorph X Y) (e' : PartialHomeomorph Y Z) : (e.trans e').symm = e'.symm.trans e.symm

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

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

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

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

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

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

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

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

theorem PartialHomeomorph.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 : PartialHomeomorph X Y) (e' : PartialHomeomorph Y Z) (e'' : PartialHomeomorph Z Z') : (e.trans e').trans e'' = e.trans (e'.trans e'')

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

theorem PartialHomeomorph.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 PartialHomeomorph.restr_trans {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph X Y) (e' : PartialHomeomorph Y Z) (s : Set X) : (e.restr s).trans e' = (e.trans e').restr s

EqOnSource: equivalence on their source

def PartialHomeomorph.EqOnSource {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : PartialHomeomorph 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 PartialHomeomorph.eqOnSource_iff {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : PartialHomeomorph X Y) : e.EqOnSource e' ↔ e.EqOnSource e'.toPartialEquiv

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

EqOnSource is an equivalence relation.

Equations

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

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

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

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

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

Two equivalent partial homeomorphisms have the same source.

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

Two equivalent partial homeomorphisms have the same target.

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

Two equivalent partial homeomorphisms have coinciding toFun on the source

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

Two equivalent partial homeomorphisms have coinciding invFun on the target

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

Composition of partial homeomorphisms respects equivalence.

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

Restriction of partial homeomorphisms respects equivalence

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

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

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

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

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

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

product of two partial homeomorphisms

def PartialHomeomorph.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 : PartialHomeomorph X X') (eY : PartialHomeomorph Y Y') : PartialHomeomorph (X × Y) (X' × Y')

The product of two partial homeomorphisms, as a 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 PartialHomeomorph.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 : PartialHomeomorph X X') (eY : PartialHomeomorph Y Y') : ↑(eX.prod eY) = fun (p : X × Y) => (↑eX p.1, ↑eY p.2)

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X X') (eY : PartialHomeomorph Y Y') : (eX.prod eY).toPartialEquiv = eX.prod eY.toPartialEquiv

theorem PartialHomeomorph.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 : PartialHomeomorph X X') (eY : PartialHomeomorph Y Y') : (eX.prod eY).source = eX.source ×ˢ eY.source

theorem PartialHomeomorph.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 : PartialHomeomorph X X') (eY : PartialHomeomorph Y Y') (p : X' × Y') : ↑(eX.prod eY).symm p = (↑eX.symm p.1, ↑eY.symm p.2)

theorem PartialHomeomorph.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 : PartialHomeomorph X X') (eY : PartialHomeomorph Y Y') : (eX.prod eY).target = eX.target ×ˢ eY.target

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X X') (eY : PartialHomeomorph Y Y') : (eX.prod eY).symm = eX.symm.prod eY.symm

@[simp]

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

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X Y) (f : PartialHomeomorph Y Z) (e' : PartialHomeomorph X' Y') (f' : PartialHomeomorph Y' Z') : (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')

theorem PartialHomeomorph.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' : PartialHomeomorph X X'} {eY eY' : PartialHomeomorph Y Y'} (h : (eX.prod eY).source.Nonempty) : eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

theorem PartialHomeomorph.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' : PartialHomeomorph X X'} {eY eY' : PartialHomeomorph Y Y'} (h : (eX'.prod eY').source.Nonempty) : eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

finite product of partial homeomorphisms

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

The product of a finite family of PartialHomeomorphs.

Equations

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

@[simp]

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

combining two partial homeomorphisms using Set.piecewise

def PartialHomeomorph.piecewise {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : PartialHomeomorph 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)) : PartialHomeomorph X Y

Combine two PartialHomeomorphs using Set.piecewise. The source of the new PartialHomeomorph 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 PartialHomeomorph.piecewise_toPartialEquiv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : PartialHomeomorph 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 PartialHomeomorph.piecewise_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : PartialHomeomorph 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 PartialHomeomorph.symm_piecewise {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : PartialHomeomorph 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 PartialHomeomorph.disjointUnion {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e e' : PartialHomeomorph 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) : PartialHomeomorph X Y

Combine two PartialHomeomorphs with disjoint sources and disjoint targets. We reuse PartialHomeomorph.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 PartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph 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 PartialHomeomorph.continuousAt_iff_continuousAt_comp_right {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph 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 a partial homeomorphism, if the point is in its target

theorem PartialHomeomorph.continuousOn_iff_continuousOn_comp_right {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph 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 a partial homeomorphism on the right is continuous on the corresponding set.

theorem PartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph 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 PartialHomeomorph.continuousAt_iff_continuousAt_comp_left {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph 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 a partial homeomorphism if a neighborhood of the initial point is sent to the source of the partial homeomorphism

theorem PartialHomeomorph.continuousOn_iff_continuousOn_comp_left {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph 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 a partial homeomorphism on the left is continuous on the corresponding set.

theorem PartialHomeomorph.continuous_iff_continuous_comp_left {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph 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 a partial homeomorphism on the left is continuous and its image is contained in the source.

def PartialHomeomorph.homeomorphOfImageSubsetSource {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) : ↑s ≃ₜ ↑t

The homeomorphism obtained by restricting a PartialHomeomorph to a subset of the source.

Equations

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

@[simp]

theorem PartialHomeomorph.homeomorphOfImageSubsetSource_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) (a✝ : ↑t) : (e.homeomorphOfImageSubsetSource hs ht).symm a✝ = Set.MapsTo.restrict (↑e.symm) t s ⋯ a✝

@[simp]

theorem PartialHomeomorph.homeomorphOfImageSubsetSource_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) (a✝ : ↑s) : (e.homeomorphOfImageSubsetSource hs ht) a✝ = Set.MapsTo.restrict (↑e) s t ⋯ a✝

def PartialHomeomorph.toHomeomorphSourceTarget {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : ↑e.source ≃ₜ ↑e.target

A partial homeomorphism defines a homeomorphism between its source and target.

Equations

• e.toHomeomorphSourceTarget = e.homeomorphOfImageSubsetSource ⋯ ⋯

@[simp]

theorem PartialHomeomorph.toHomeomorphSourceTarget_symm_apply_coe {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (a✝ : ↑e.target) : ↑(e.toHomeomorphSourceTarget.symm a✝) = ↑e.symm ↑a✝

@[simp]

theorem PartialHomeomorph.toHomeomorphSourceTarget_apply_coe {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (a✝ : ↑e.source) : ↑(e.toHomeomorphSourceTarget a✝) = ↑e ↑a✝

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

theorem PartialHomeomorph.nhds_eq_comap_inf_principal {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {x : X} (hx : x ∈ e.source) : nhds x = Filter.comap (↑e) (nhds (↑e x)) ⊓ Filter.principal e.source

def PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ) : X ≃ₜ Y

If a partial homeomorphism has source and target equal to univ, then it induces a homeomorphism between the whole spaces, expressed in this definition.

Equations

• e.toHomeomorphOfSourceEqUnivTargetEqUniv h h' = { toFun := ↑e, invFun := ↑e.symm, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ) : ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h') = ↑e

@[simp]

theorem PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (h : e.source = Set.univ) (h' : e.target = Set.univ) : ⇑(e.toHomeomorphOfSourceEqUnivTargetEqUniv h h').symm = ↑e.symm

theorem PartialHomeomorph.isOpenEmbedding_restrict {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Topology.IsOpenEmbedding (e.source.restrict ↑e)

@[deprecated PartialHomeomorph.isOpenEmbedding_restrict (since := "2024-10-18")]

theorem PartialHomeomorph.openEmbedding_restrict {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) : Topology.IsOpenEmbedding (e.source.restrict ↑e)

Alias of PartialHomeomorph.isOpenEmbedding_restrict.

theorem PartialHomeomorph.to_isOpenEmbedding {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (h : e.source = Set.univ) : Topology.IsOpenEmbedding ↑e

A partial homeomorphism whose source is all of X defines an open embedding of X into Y. The converse is also true; see IsOpenEmbedding.toPartialHomeomorph.

@[deprecated PartialHomeomorph.to_isOpenEmbedding (since := "2024-10-18")]

theorem PartialHomeomorph.to_openEmbedding {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) (h : e.source = Set.univ) : Topology.IsOpenEmbedding ↑e

Alias of PartialHomeomorph.to_isOpenEmbedding.

---

A partial homeomorphism whose source is all of X defines an open embedding of X into Y. The converse is also true; see IsOpenEmbedding.toPartialHomeomorph.

@[simp]

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

@[simp]

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

@[simp]

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').toPartialHomeomorph = e.toPartialHomeomorph.trans e'.toPartialHomeomorph

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' : PartialHomeomorph Y Z) : PartialHomeomorph X Z

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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' : PartialHomeomorph Y Z) : e.transPartialHomeomorph f' = e.toPartialHomeomorph.trans f'

@[simp]

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 : PartialHomeomorph Y Z) (f' : PartialHomeomorph Z Z') : (e.transPartialHomeomorph f).trans f' = e.transPartialHomeomorph (f.trans f')

@[simp]

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'' : PartialHomeomorph Z Z') : (e.trans e').transPartialHomeomorph f'' = e.transPartialHomeomorph (e'.transPartialHomeomorph f'')

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

An open embedding of X into Y, with X nonempty, defines a partial homeomorphism whose source is all of X. The converse is also true; see PartialHomeomorph.to_isOpenEmbedding.

Equations

• Topology.IsOpenEmbedding.toPartialHomeomorph f h = PartialHomeomorph.ofContinuousOpen (Set.InjOn.toPartialEquiv f Set.univ ⋯) ⋯ ⋯ ⋯

@[simp]

theorem Topology.IsOpenEmbedding.toPartialHomeomorph_source {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] : (toPartialHomeomorph f h).source = Set.univ

@[simp]

theorem Topology.IsOpenEmbedding.toPartialHomeomorph_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] : ↑(toPartialHomeomorph f h) = f

@[simp]

theorem Topology.IsOpenEmbedding.toPartialHomeomorph_target {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (h : IsOpenEmbedding f) [Nonempty X] : (toPartialHomeomorph f h).target = Set.range f

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} : ↑(toPartialHomeomorph f h).symm (f x) = x

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 (↑(toPartialHomeomorph f h).symm x) = x

inclusion of an open set in a topological space

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

The inclusion of an open subset s of a space X into X is a partial homeomorphism from the subtype s to X.

Equations

• s.partialHomeomorphSubtypeCoe hs = Topology.IsOpenEmbedding.toPartialHomeomorph Subtype.val ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

Postcompose a 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 PartialHomeomorph.transHomeomorph_apply {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : PartialHomeomorph X Y) (f' : Y ≃ₜ Z) : ↑(e.transHomeomorph f') = ⇑f' ∘ ↑e

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X Y) (f' : Y ≃ₜ Z) (f'' : Z ≃ₜ Z') : (e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'')

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X Y) (e' : PartialHomeomorph Y Z) (f'' : Z ≃ₜ Z') : (e.trans e').transHomeomorph f'' = e.trans (e'.transHomeomorph f'')

subtypeRestr: restriction to a subtype

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

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

Equations

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

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

@[simp]

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

@[simp]

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

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

theorem PartialHomeomorph.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' : PartialHomeomorph 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 PartialHomeomorph.subtypeRestr_symm_eqOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {U : TopologicalSpace.Opens X} (hU : Nonempty ↥U) : Set.EqOn (↑e.symm) (Subtype.val ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target

theorem PartialHomeomorph.subtypeRestr_symm_eqOn_of_le {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph 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 PartialHomeomorph.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 : PartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : PartialHomeomorph X' Z

Extend a 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 PartialHomeomorph.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 : PartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : ↑(e.lift_openEmbedding hf) = Function.extend f ↑e fun (x : X') => Classical.arbitrary Z

theorem PartialHomeomorph.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 : PartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) {x : X} : ↑(e.lift_openEmbedding hf) (f x) = ↑e x

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).source = f '' e.source

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).target = e.target

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : ↑(e.lift_openEmbedding hf).symm = f ∘ ↑e.symm

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).symm.source = e.target

@[simp]

theorem PartialHomeomorph.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 : PartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).symm.target = f '' e.source

theorem PartialHomeomorph.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' : PartialHomeomorph 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 PartialHomeomorph.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' : PartialHomeomorph X Z) (hf : Topology.IsOpenEmbedding f) : (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) = e.symm.trans e'