Partial homeomorphisms: composition #

Main definitions #

OpenPartialHomeomorph.trans: the composition of two open partial homeomorphisms

Composition #

trans: composition of two open partial homeomorphisms

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

OpenPartialHomeomorph X Z

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

Equations

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

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) (h : e.target = e'.source) :

(e.trans' e' h).toPartialEquiv = e.trans' e'.toPartialEquiv h

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

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

This could be considered as a simp lemma, but there are many situations where it makes something simple into something more complicated.

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

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

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

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

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

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

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

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

Documentation

Mathlib.Topology.OpenPartialHomeomorph.Composition

Partial homeomorphisms: composition #

Main definitions #

Composition #