Constructions of new partial homeomorphisms from old

Main definitions

• OpenPartialHomeomorph.const: an open partial homeomorphism which is a constant map, whose source and target are necessarily singleton sets
• OpenPartialHomeomorph.subtypeRestr: restriction to a subtype
• 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.)

Constants

PartialEquiv.const as an open partial homeomorphism

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

Products

Product of two open partial homeomorphisms

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem OpenPartialHomeomorph.prod_symm_trans_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'] (e f : OpenPartialHomeomorph X Y) (e' f' : OpenPartialHomeomorph X' Y') : (e.prod e').symm.trans (f.prod f') = (e.symm.trans f).prod (e'.symm.trans f')

Pi types

Finite indexed products of partial homeomorphisms

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

The product of a finite family of OpenPartialHomeomorphs.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem OpenPartialHomeomorph.pi_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)

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

Disjoint union

Combining two partial homeomorphisms using Set.piecewise

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem OpenPartialHomeomorph.transHomeomorph_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

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

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

@[simp]

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

@[simp]

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

Restriction to a subtype

subtypeRestr: restriction to a subtype

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

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

Equations

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

Extending along an open embedding

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

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

Equations

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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