instContinuousEvalConst — Mathlib

English

There is a continuous evaluation-constant structure on C(X,R)₀, obtained from the embedding into C(X,R). In particular, the evaluation at a fixed x is continuous.

Русский

Существуют константы непрерывной оценки на C(X,R)₀, полученные через вложение в C(X,R); в частности, отображение f ↦ f(x) непрерывно.

LaTeX

$$$\\text{ContinuousEvalConst } C(X,R)_0$ and for each $x\\in X$, the evaluation map $f\\mapsto f(x)$ is continuous.$$

Lean4

instance instContinuousEvalConst : ContinuousEvalConst C(X, R)₀ X R :=
  .of_continuous_forget isEmbedding_toContinuousMap.continuous

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