English
The map (f,g) ↦ g ∘ f is continuous from C(X,Y) × C(Y,Z) to C(X,Z) provided Y is locally compact.
Русский
Отображение (f,g) ↦ g ∘ f неприменимо на C(X,Y) × C(Y,Z) в C(X,Z) при локально компактных Y.
LaTeX
$$$\\text{Continuous}'(f,g)\\mapsto g\\circ f$ is continuous, when $Y$ is locally compact.$$
Lean4
/-- Composition is a continuous map from `C(X, Y) × C(Y, Z)` to `C(X, Z)`,
provided that `Y` is locally compact.
This is Prop. 9 of Chap. X, §3, №. 4 of Bourbaki's *Topologie Générale*. -/
theorem continuous_comp' : Continuous fun x : C(X, Y) × C(Y, Z) => x.2.comp x.1 :=
by
simp_rw [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_compactOpen]
intro ⟨f, g⟩ K hK U hU (hKU : MapsTo (g ∘ f) K U)
obtain ⟨L, hKL, hLc, hLU⟩ : ∃ L ∈ 𝓝ˢ (f '' K), IsCompact L ∧ MapsTo g L U :=
exists_mem_nhdsSet_isCompact_mapsTo g.continuous (hK.image f.continuous) hU (mapsTo_image_iff.2 hKU)
rw [← subset_interior_iff_mem_nhdsSet, ← mapsTo_iff_image_subset] at hKL
exact
((eventually_mapsTo hK isOpen_interior hKL).prod_nhds (eventually_mapsTo hLc hU hLU)).mono fun ⟨f', g'⟩ ⟨hf', hg'⟩ ↦
hg'.comp <| hf'.mono_right interior_subset
