English
The restricted lifting map liftCM(T) is a continuous map from the product of the source with the base set to the source, sending (p, ex) to T.lift p ex.
Русский
Ограниченная функция LiftCM(T) — непрерывное отображение из произведения источника и базового множества в источник, отправляющее (p, ex) в T.lift p ex.
LaTeX
$$$$\mathrm{liftCM}(T)\;:\;T.source\times T.baseSet\to T.source,\quad (ex)\mapsto T.lift(ex.1,ex.2).$$$$
Lean4
/-- The restriction of `lift` to the source and base set of `T`, as a bundled continuous map. -/
def liftCM (T : Trivialization F proj) : C(T.source × T.baseSet, T.source)
where
toFun ex := ⟨T.lift ex.1 ex.2, T.map_target (by simp [mem_target])⟩
continuous_toFun := by
apply Continuous.subtype_mk
refine T.continuousOn_invFun.comp_continuous ?_ (by simp [mem_target])
refine .prodMk (by fun_prop) (.snd ?_)
exact T.continuousOn_toFun.comp_continuous (by fun_prop) (by simp)
