English
There is a natural continuous map sending a point x ∈ X to the evaluation character on C(X, 𝕜), i.e., x ↦ ev_x which evaluates a function at x.
Русский
Существует естественное непрерывное отображение, отправляющее точку x ∈ X в функционал оценки на C(X, 𝕜), то есть x ↦ ev_x, который берёт значение функции в точке x.
LaTeX
$$There exists a continuous map x ↦ ev_x : X → WeakDual.CharacterSpace 𝕜 (C(X, 𝕜)).Elem$$
Lean4
/-- The natural continuous map from a locally compact topological space `X` to the
`WeakDual.characterSpace 𝕜 C(X, 𝕜)` which sends `x : X` to point evaluation at `x`. -/
def continuousMapEval : C(X, characterSpace 𝕜 C(X, 𝕜))
where
toFun
x :=
⟨{ toFun := fun f => f x
map_add' := fun _ _ => rfl
map_smul' := fun _ _ => rfl
cont := continuous_eval_const x }, by rw [CharacterSpace.eq_set_map_one_map_mul]; exact ⟨rfl, fun f g => rfl⟩⟩
continuous_toFun := by exact Continuous.subtype_mk (continuous_of_continuous_eval map_continuous) _
