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.

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

@[simp]

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

@[simp]

theorem OpenPartialHomeomorph.trans'_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✝)

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

Composition of open partial homeomorphisms respects equivalence.

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

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

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

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

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

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

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.

@[simp]

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

@[simp]

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

@[simp]

theorem Homeomorph.transOpenPartialHomeomorph_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

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

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'

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

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