Gluing two maps along the halves of a parameter

Given a continuous parameter s : C(Z, I) and two maps a, a' : C(Z, X) that agree where s = 1/2, ContinuousMap.glueHalves s a a' is a on s ≤ 1/2 and a' on 1/2 ≤ s.

Main definitions

• ContinuousMap.glueHalves: the glued map, with the evaluation lemmas ContinuousMap.glueHalves_of_le and ContinuousMap.glueHalves_of_not_le.

noncomputable def ContinuousMap.glueHalves {Z : Type u_1} {X : Type u_2} [TopologicalSpace Z] [TopologicalSpace X] (s : C(Z, ↑unitInterval)) (a a' : C(Z, X)) (h : ∀ (z : Z), ↑(s z) = 2⁻¹ → a z = a' z) : C(Z, X)

Glue two maps along the two halves s ≤ 1/2 and 1/2 ≤ s of the parameter s, assuming that they agree where s = 1/2.

@[simp]

theorem ContinuousMap.glueHalves_of_le {Z : Type u_1} {X : Type u_2} [TopologicalSpace Z] [TopologicalSpace X] (s : C(Z, ↑unitInterval)) (a a' : C(Z, X)) (h : ∀ (z : Z), ↑(s z) = 2⁻¹ → a z = a' z) {z : Z} (hz : ↑(s z) ≤ 2⁻¹) : (s.glueHalves a a' h) z = a z

@[simp]

theorem ContinuousMap.glueHalves_of_not_le {Z : Type u_1} {X : Type u_2} [TopologicalSpace Z] [TopologicalSpace X] (s : C(Z, ↑unitInterval)) (a a' : C(Z, X)) (h : ∀ (z : Z), ↑(s z) = 2⁻¹ → a z = a' z) {z : Z} (hz : ¬↑(s z) ≤ 2⁻¹) : (s.glueHalves a a' h) z = a' z