English
If f is a quotient map X0 → X and Gf := curry(hg) is continuous in the curried form, then the lift yields continuity of g on X × Y.
Русский
Пусть f — тождественная карта X0 → X. Если отображение hg есть непрерывное после карриирования, то линейный подъём даёт непрерывность g на X × Y.
LaTeX
$$$(\\text{hf} : \\text{IsQuotientMap } f) \\Rightarrow (\\text{Continuous}(p \\mapsto g(f(p.1), p.2)) \\Rightarrow \\text{Continuous } g)$$$
Lean4
theorem continuous_lift_prod_left (hf : IsQuotientMap f) {g : X × Y → Z}
(hg : Continuous fun p : X₀ × Y => g (f p.1, p.2)) : Continuous g :=
by
let Gf : C(X₀, C(Y, Z)) := ContinuousMap.curry ⟨_, hg⟩
have h : ∀ x : X, Continuous fun y => g (x, y) := by
intro x
obtain ⟨x₀, rfl⟩ := hf.surjective x
exact (Gf x₀).continuous
let G : X → C(Y, Z) := fun x => ⟨_, h x⟩
have : Continuous G := by
rw [hf.continuous_iff]
exact Gf.continuous
exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩
