continuous_eval_const — Mathlib

English

The edist between f and g equals the supremum of the pointwise edistances.

Русский

Edist между f и g равен супремуму по точкам Edist(f(x),g(x)).

LaTeX

$$$\\operatorname{edist} f g = \\sup_{x \\in \\alpha} \\operatorname{edist}(f x, g x).$$$

Lean4

/-- When `x` is fixed, `(f : α →ᵇ β) ↦ f x` is continuous. -/
@[continuity]
theorem continuous_eval_const {x : α} : Continuous fun f : α →ᵇ β => f x :=
  (continuous_apply x).comp continuous_coe

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