uniformContinuous_eval_const — Mathlib

English

Fixing a coordinate function x ∈ ι → E, the evaluation map that sends f to f(x) is uniformly continuous.

Русский

При фиксированной координатной функции x ∈ ι → E отображение оценки, отправляющее f на f(x), равномерно непрерывно.

LaTeX

$$$$ UniformContinuous (\\lambda f: E [⋀^ι]→L[𝕜] F \\mapsto f(x)). $$$$

Lean4

theorem uniformContinuous_eval_const [ContinuousSMul 𝕜 E] (x : ι → E) :
    UniformContinuous fun f : E [⋀^ι]→L[𝕜] F ↦ f x :=
  uniformContinuous_pi.1 uniformContinuous_coe_fun x

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