continuous_eval — Mathlib

English

Convergence in the topology of bounded continuous functions is equivalent to uniform convergence on α.

Русский

Сходимость в топологии ограниченных непрерывных функций эквивалентна равномерной сходимости на α.

LaTeX

$$$\\operatorname{Tendsto} F\\,l\\,(\\mathcal{N} f) \iff \\operatorname{TendstoUniformly} F f l$$$

Lean4

/-- The evaluation map is continuous, as a joint function of `u` and `x`. -/
@[continuity]
theorem continuous_eval : Continuous fun p : (α →ᵇ β) × α => p.1 p.2 :=
  (continuous_prod_of_continuous_lipschitzWith _ 1 fun f => f.continuous) <| lipschitz_evalx

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