instContinuousEval — Mathlib

English

If (X,R) form a LocallyCompactPair, then C(X,R)₀ admits a continuous evaluation: the map f ↦ f(x) is continuous for each x.

Русский

Для локально компактной пары (X,R) отображение f ↦ f(x) непрерывно для каждого x.

LaTeX

$$$[LocallyCompactPair\\ X\\ R] \\Rightarrow \\text{ContinuousEval } C(X,R)_0$$$

Lean4

instance instContinuousEval [LocallyCompactPair X R] : ContinuousEval C(X, R)₀ X R :=
  .of_continuous_forget isEmbedding_toContinuousMap.continuous

Похожие утверждения