English
Extend liftCM to a map clift that takes a base map valued in T.baseSet and produces a continuous map valued in T.source, by composing with liftCM and directing via appropriate coordinate changes.
Русский
Расширяем liftCM до отображения clift, которое принимает непрерывные карты в T.baseSet и даёт непрерывную карту в T.source, за счёт компоновки с liftCM и соответствующих преобразований координат.
LaTeX
$$$$\mathrm{clift}(T) : C\bigl(T^{\mathrm{source}}\times C(\iota, T.baseSet), T^{\mathrm{source}}\bigr).$$$$
Lean4
/-- Extension of `liftCM` to continuous maps taking values in `T.baseSet` (local version of
homotopy lifting) -/
def clift (T : Trivialization F proj) [LocallyCompactPair ι T.baseSet] :
C(T.source × C(ι, T.baseSet), C(ι, T.source)) :=
by
let Ψ : C((T.source × C(ι, T.baseSet)) × ι, C(ι, T.baseSet) × ι) := ⟨fun eγt => (eγt.1.2, eγt.2), by fun_prop⟩
refine ContinuousMap.curry <| T.liftCM.comp <| ⟨fun eγt => ⟨eγt.1.1, eγt.1.2 eγt.2⟩, ?_⟩
simpa using ⟨by fun_prop, ContinuousEval.continuous_eval.comp Ψ.continuous⟩
