English
The evaluation map ev: C(X,Y) × X → Y, (f,x) ↦ f(x), is continuous when X,Y form a locally compact pair.
Русский
Оценочная карта ev: C(X,Y) × X → Y, (f,x) ↦ f(x), непрерывна при пары X,Y, которая локально компактна.
LaTeX
$$$\\text{ContinuousEval } C(X,Y)\\,X\\,Y$;\\ ev: C(X,Y) \\times X \\to Y \text{ is continuous}$$
Lean4
/-- The evaluation map `C(X, Y) × X → Y` is continuous
if `X, Y` is a locally compact pair of spaces. -/
instance [LocallyCompactPair X Y] : ContinuousEval C(X, Y) X Y where
continuous_eval :=
by
simp_rw [continuous_iff_continuousAt, ContinuousAt, (nhds_basis_opens _).tendsto_right_iff]
rintro ⟨f, x⟩ U ⟨hx : f x ∈ U, hU : IsOpen U⟩
rcases exists_mem_nhds_isCompact_mapsTo f.continuous (hU.mem_nhds hx) with ⟨K, hxK, hK, hKU⟩
filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2
