English
The map p: X × C(Y, Z) → C(Y, X × Z) given by p(x, f)(y) = (x, f(y)) is continuous.
Русский
Отображение p: X × C(Y,Z) → C(Y,X×Z), определяемое p(x,f)(y) = (x,f(y)), непрерывно.
LaTeX
$$$\\text{Continuous } p,\\, p(x,f)(y)=(x,f(y))$$$
Lean4
/-- The map from `X × C(Y, Z)` to `C(Y, X × Z)` is continuous. -/
theorem continuous_prodMk_const : Continuous fun p : X × C(Y, Z) ↦ prodMk (const Y p.1) p.2 :=
by
simp_rw [continuous_iff_continuousAt, ContinuousAt, ContinuousMap.tendsto_nhds_compactOpen]
rintro ⟨r, f⟩ K hK U hU H
obtain ⟨V, W, hV, hW, hrV, hKW, hVW⟩ :=
generalized_tube_lemma (isCompact_singleton (x := r)) (hK.image f.continuous) hU
(by simpa [Set.subset_def, forall_comm (α := X)])
refine
Filter.eventually_of_mem
(prod_mem_nhds (hV.mem_nhds (by simpa using hrV))
(ContinuousMap.eventually_mapsTo hK hW (Set.mapsTo_iff_image_subset.mpr hKW)))
?_
rintro ⟨r', f'⟩ ⟨hr'V, hf'⟩ x hxK
exact hVW (Set.mk_mem_prod hr'V (hf' hxK))
