Composing and restricting open partial homeomorphisms

This file supplements Mathlib.Topology.OpenPartialHomeomorph.Composition:

• OpenPartialHomeomorph.image_trans_source_inter, OpenPartialHomeomorph.image_restrOpen_source_inter, OpenPartialHomeomorph.image_symm_trans_source_inter, and OpenPartialHomeomorph.image_restrOpen_symm_trans_source_inter: equational image-transport formulas for compositions e.trans e', open restrictions e.restrOpen u hu, and chart transitions e.symm.trans e'.
• Homeomorph.refl_transOpenPartialHomeomorph: precomposing an open partial homeomorphism with Homeomorph.refl changes nothing; together with Homeomorph.trans_transOpenPartialHomeomorph this makes Homeomorph.transOpenPartialHomeomorph an action of homeomorphisms.

theorem OpenPartialHomeomorph.image_trans_source_inter {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z) (s : Set X) : ↑(e.trans e') '' ((e.trans e').source ∩ s) = ↑e' '' (e'.source ∩ ↑e '' (e.source ∩ s))

Pushing a set forward along a composition e.trans e' of open partial homeomorphisms pushes its e-source trace through e and then its e'-source trace through e'.

theorem OpenPartialHomeomorph.image_restrOpen_source_inter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : OpenPartialHomeomorph X Y) {u : Set X} (hu : IsOpen u) (s : Set X) : ↑(e.restrOpen u hu) '' ((e.restrOpen u hu).source ∩ s) = (e.restrOpen u hu).target ∩ ↑e '' (e.source ∩ s)

Restricting an open partial homeomorphism to an open subset u intersects source-restricted images with the restricted target.

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

A transition open partial homeomorphism e.symm.trans e' transports the e-image of s onto the part of the e'-image of s lying in (e.symm.trans e').target.

theorem OpenPartialHomeomorph.image_restrOpen_symm_trans_source_inter {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph X Z) {u : Set Y} (hu : IsOpen u) (s : Set X) : ↑((e.symm.trans e').restrOpen u hu) '' (((e.symm.trans e').restrOpen u hu).source ∩ ↑e '' (e.source ∩ s)) = ((e.symm.trans e').restrOpen u hu).target ∩ ↑e' '' (e'.source ∩ s)

Restricting a transition open partial homeomorphism e.symm.trans e' to an open subset u ⊆ Y transports the e-image of s onto the part of the e'-image of s lying in ((e.symm.trans e').restrOpen u hu).target.

@[simp]

theorem Homeomorph.refl_transOpenPartialHomeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (c : OpenPartialHomeomorph X Y) : (Homeomorph.refl X).transOpenPartialHomeomorph c = c

Precomposing an open partial homeomorphism with the identity homeomorphism leaves it unchanged.