Homotopy with a predicate is path connectedness

Mathlib's ContinuousMap.HomotopicWith f g P asks for a homotopy from f to g all of whose stages satisfy P. This file proves that, under LocallyCompactPair X Y (for instance, when the domain is locally compact), this is exactly path connectedness of f and g in the subspace {h : C(X, Y) // P h} of the compact-open topology: currying a homotopy gives the path, and uncurrying a path gives the homotopy.

Main declarations

• ContinuousMap.homotopicWith_iff_joined: f.HomotopicWith g P holds exactly when f and g are joined by a path in {h : C(X, Y) // P h}.

theorem ContinuousMap.homotopicWith_iff_joined {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y) → Prop} [LocallyCompactPair X Y] {f g : C(X, Y)} (hf : P f) (hg : P g) : f.HomotopicWith g P ↔ Joined ⟨f, hf⟩ ⟨g, hg⟩

Homotopy through maps satisfying P is path connectedness in {h : C(X, Y) // P h}, under LocallyCompactPair X Y (for instance, for a locally compact domain).