Evaluating a homotopy fixing a set at a variable time

Let h : T × Y → Y, with T compact, fix every point of a set A ⊆ Y at all times. Evaluating h at a time φ z and a point q z gives a continuous function of z as soon as q is continuous and φ is continuous at the points with q z ∉ A; nothing is required of φ over A. This is a tube-lemma argument over the compact parameter space T.

Such times typically have the form min 1 (t / u y) for a control function u : Y → I vanishing exactly on A, which is discontinuous at A but continuous off it. The file records that continuity, together with the fact that the real value of such a control function is nonzero off A.

Main declarations

• ContinuousMap.continuous_apply_prodMk_of_fixed: a homotopy fixing A, evaluated at a time that is continuous away from A, is continuous.
• TauCeti.coe_ne_zero_iff_notMem: a function to I vanishing exactly on A has nonzero real value exactly off A.
• ContinuousMap.continuousAt_projIcc_div_of_notMem: the time min 1 (t / u y), as a point of I, is continuous off the zero set of u.

theorem ContinuousMap.continuous_apply_prodMk_of_fixed {T : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace T] [TopologicalSpace Y] [TopologicalSpace Z] [CompactSpace T] (h : C(T × Y, Y)) {A : Set Y} (hA : ∀ (t : T), ∀ y ∈ A, h (t, y) = y) {q : Z → Y} (hq : Continuous q) {φ : Z → T} (hφ : ∀ (z : Z), q z ∉ A → ContinuousAt φ z) : Continuous fun (z : Z) => h (φ z, q z)

Let h : T × Y → Y, with T compact, fix every point of A at all times. Then evaluating h at a point q z and at a time φ z gives a continuous function of z, as soon as q is continuous and φ is continuous at the points z with q z ∉ A. No condition on φ is needed over A: by compactness of T, near a point of A all the values h (t, y) are close to it.

theorem TauCeti.coe_ne_zero_iff_notMem {X : Type u_1} {A : Set X} {u : X → ↑unitInterval} (hu : ∀ (x : X), u x = 0 ↔ x ∈ A) (x : X) : ↑(u x) ≠ 0 ↔ x ∉ A

A function u : X → I vanishing exactly on A has nonzero real value exactly off A.

theorem ContinuousMap.continuousAt_projIcc_div_of_notMem {X : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Z] {A : Set X} (u : C(X, ↑unitInterval)) (hu : ∀ (x : X), u x = 0 ↔ x ∈ A) {t : Z → ↑unitInterval} {q : Z → X} (ht : Continuous t) (hq : Continuous q) {z : Z} (hz : q z ∉ A) : ContinuousAt (fun (z : Z) => Set.projIcc 0 1 ⋯ (↑(t z) / ↑(u (q z)))) z

Let u : X → I be continuous and vanish exactly on A. Then the time min 1 (t z / u (q z)), as a point of I, is continuous at every z with q z ∉ A, for continuous t : Z → I and q : Z → X.