English
If p is a local homeomorphism and separated, and if a lift g of a map f is given with g restricted to 0 and to a fixed a, then the lifted map g is continuous.
Русский
Если p — локальный гомеоморфизм и разнесённая пара, и дано поднятие g отображения f, причём g ограничено на начальный момент и фиксированное значение a, тогда подъем g непрерывен.
LaTeX
$$$$\text{Let } p:\,E\to X \text{ be a local homeomorphism and separated. For } f\in C(I\times A, X) \text{ and } g:I\times A\to E \text{ with } p\circ g=f,\; (cont_0, cont_A)$$ $$\text{then } g \text{ is continuous.}$$$$
Lean4
theorem continuous_lift (f : C(I × A, X)) {g : I × A → E} (g_lifts : p ∘ g = f) (cont_0 : Continuous (g ⟨0, ·⟩))
(cont_A : ∀ a, Continuous (g ⟨·, a⟩)) : Continuous g :=
by
rw [continuous_iff_continuousAt]
intro ⟨t, a⟩
obtain ⟨N, haN, g', cont_g', g'_lifts, g'_0, -⟩ := homeo.exists_lift_nhds g_lifts cont_0 a (cont_A a)
refine (cont_g'.congr fun ⟨t, a⟩ ⟨_, ha⟩ ↦ ?_).continuousAt (prod_mem_nhds Filter.univ_mem haN)
refine
congr_fun
(sep.eq_of_comp_eq homeo.isLocallyInjective (cont_A a) (cont_g'.comp_continuous (.prodMk_left a) fun _ ↦ ⟨⟨⟩, ha⟩)
?_ 0 (g'_0 a).symm)
t
ext t; apply congr_fun (g_lifts.trans g'_lifts.symm)
