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

source
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

Instances For

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

Instances For

Basic properties; inverse (symm instance)

source
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

Instances For

source
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 }

source
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 := ⋯ }

Instances For

source
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

Instances For

source
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

Instances For

source
theorem OpenPartialHomeomorph.continuousOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) :
ContinuousOn (↑e) e.source
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
source
@[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
source
@[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
source
theorem OpenPartialHomeomorph.toPartialEquiv_injective {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] :
Function.Injective toPartialEquiv
source
@[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
source
@[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
source
@[simp]
theorem OpenPartialHomeomorph.coe_coe {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) :
↑e.toPartialEquiv = ↑e
source
@[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
source
@[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
source
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`.

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
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
source
@[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
source
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
source
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
source
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
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
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
source
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
source
theorem OpenPartialHomeomorph.injOn {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) :
Set.InjOn (↑e) e.source
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
source
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
source
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 := ⋯ }

Instances For

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

Instances For

source
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 ⋯

Instances For

source
@[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
source
@[simp]
theorem Homeomorph.toOpenPartialHomeomorph_apply {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) :
↑e.toOpenPartialHomeomorph = ⇑e
source
@[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
source
@[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
source
@[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

Instances For

source
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 := ⋯ }

Instances For

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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)
source
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
source
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)
source
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
source
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
source
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
source
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
source
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
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`.

source
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
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
source
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
source
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
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
source
theorem OpenPartialHomeomorph.symm_bijective {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] :
Function.Bijective OpenPartialHomeomorph.symm
source
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

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

source
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)
source
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)
source
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
source
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)
source
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))
source
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
source
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)
source
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
source
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)
source
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
source
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`).

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

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

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

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

source
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)

Instances For

source
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
source
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
source
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
source
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
source
@[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
source
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)
source
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)
source
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
source
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
source
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
source
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`.

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

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

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

source
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
source
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'`.

source
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'`.

source
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
source
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'`.

source
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'`.

source
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
source
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
source
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 ᶜ
source
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')
source
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')
source
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')
source
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)
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
source
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)
source
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
source
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)
source
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)
source
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)
source
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)
source
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 := ⋯ }

Instances For

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

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)
source
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)
source
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 := ⋯ }

Instances For

source
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

Instances For

source
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 ⋯

Instances For

source
@[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
source
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
source
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) ⋯

Instances For

source
@[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
source
@[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
source
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
source
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
source
@[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)
source
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
source
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
source
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
source
@[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
source
@[simp]
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
source
def OpenPartialHomeomorph.refl (X : Type u_7) [TopologicalSpace X] :
OpenPartialHomeomorph X X

The identity on the whole space as an open partial homeomorphism.

Equations

- OpenPartialHomeomorph.refl X = (Homeomorph.refl X).toOpenPartialHomeomorph

Instances For

source
@[simp]
theorem OpenPartialHomeomorph.refl_apply (X : Type u_7) [TopologicalSpace X] :
↑(OpenPartialHomeomorph.refl X) = id
source
theorem OpenPartialHomeomorph.refl_source (X : Type u_7) [TopologicalSpace X] :
(OpenPartialHomeomorph.refl X).source = Set.univ
source
theorem OpenPartialHomeomorph.refl_target (X : Type u_7) [TopologicalSpace X] :
(OpenPartialHomeomorph.refl X).target = Set.univ
source
@[simp]
theorem OpenPartialHomeomorph.refl_partialEquiv {X : Type u_1} [TopologicalSpace X] :
(OpenPartialHomeomorph.refl X).toPartialEquiv = PartialEquiv.refl X
source
@[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

source
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 := ⋯ }

Instances For

source
@[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
source
@[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}
source
@[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`

source
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 := ⋯ }

Instances For

source
@[simp]
theorem OpenPartialHomeomorph.ofSet_apply {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) :
↑(ofSet s hs) = id
source
theorem OpenPartialHomeomorph.ofSet_source {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) :
(ofSet s hs).source = s
source
theorem OpenPartialHomeomorph.ofSet_target {X : Type u_1} [TopologicalSpace X] (s : Set X) (hs : IsOpen s) :
(ofSet s hs).target = s
source
@[simp]
theorem OpenPartialHomeomorph.ofSet_toPartialEquiv {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :
(ofSet s hs).toPartialEquiv = PartialEquiv.ofSet s
source
@[simp]
theorem OpenPartialHomeomorph.ofSet_symm {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :
(ofSet s hs).symm = ofSet s hs
source
@[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

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) (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 := ⋯ }

Instances For

source
@[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✝)
source
@[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✝)
source
@[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
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) (h : e.target = e'.source) :
(e.trans' e' h).target = e'.target
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) (h : e.target = e'.source) :
(e.trans' e' h).source = e.source
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 ⋯) ⋯

Instances For

source
@[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
source
@[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
source
@[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
source
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)
source
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
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'.source
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)
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)
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
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
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'.source ∩ e.target)
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' '' (e'.source ∩ e.target)
source
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
source
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'')
source
@[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
source
@[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
source
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)
source
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)
source
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
source
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)
source
@[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') ⋯
source
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

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)

Instances For

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
source
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 := ⋯ }

source
theorem OpenPartialHomeomorph.eqOnSource_refl {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) :
e ≈ e
source
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.

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

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.

source
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

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

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

source
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

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

source
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

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 ⋯
source
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'
source
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)
source
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)
source
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'
source
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

source
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 := ⋯ }

Instances For

source
@[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
source
@[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)
source
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
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
source
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)
source
@[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
source
@[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)
source
@[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')
source
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'
source
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

source
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 `OpenPartialHomeomorph`s.

Equations

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

Instances For

source
@[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
source
@[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
source
@[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)
source
@[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
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`

source
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 `OpenPartialHomeomorph`s 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 := ⋯ }

Instances For

source
@[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'
source
@[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'
source
@[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 ⋯ ⋯ ⋯ ⋯
source
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 `OpenPartialHomeomorph`s 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) ⋯

Instances For

source
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

source
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

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

source
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

source
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

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

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

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.

Instances For

source
@[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✝
source
@[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✝
source
def OpenPartialHomeomorph.toHomeomorphSourceTarget {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) :
↑e.source ≃ₜ ↑e.target

An open partial homeomorphism defines a homeomorphism between its source and target.

Equations

- e.toHomeomorphSourceTarget = e.homeomorphOfImageSubsetSource ⋯ ⋯

Instances For

source
@[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✝
source
@[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✝
source
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
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
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 := ⋯ }

Instances For

source
@[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
source
@[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
source
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)
source
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`.

source
@[simp]
theorem Homeomorph.refl_toOpenPartialHomeomorph {X : Type u_1} [TopologicalSpace X] :
(Homeomorph.refl X).toOpenPartialHomeomorph = OpenPartialHomeomorph.refl X
source
@[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`.

source
@[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
source
@[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`.

source
@[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
source
@[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`.

source
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 := ⋯ }

Instances For

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

Instances For

source
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'
source
@[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`.

source
@[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')
source
@[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`.

source
@[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'')
source
@[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`.

source
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 ⋯) ⋯ ⋯ ⋯

Instances For

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

Instances For

source
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
source
@[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`.

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

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

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

Equations

- s.openPartialHomeomorphSubtypeCoe hs = Topology.IsOpenEmbedding.toOpenPartialHomeomorph Subtype.val ⋯

Instances For

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

Instances For

source
@[simp]
theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_coe {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) :
↑(s.openPartialHomeomorphSubtypeCoe hs) = Subtype.val
source
@[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`.

source
@[simp]
theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) :
(s.openPartialHomeomorphSubtypeCoe hs).source = Set.univ
source
@[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`.

source
@[simp]
theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target {X : Type u_1} [TopologicalSpace X] (s : Opens X) (hs : Nonempty ↥s) :
(s.openPartialHomeomorphSubtypeCoe hs).target = ↑s
source
@[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`.

source
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 := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
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
source
@[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'')
source
@[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

source
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

Instances For

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

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

Instances For

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