tendstoUniformly — Mathlib

English

Let f: α → β → γ be uniformly continuous in both arguments. Then as the first input tends to x, the family of functions b ↦ f(a,b) converges to f(x,·) uniformly in b.

Русский

Пусть f: α → β → γ равномерно непрерывна по обоим аргументам. Тогда при приближении первого аргумента к x семейство функций b ↦ f(a,b) сходится равномерно к f(x,b) по переменной b.

LaTeX

$$$TendstoUniformly f (f x) (\mathcal N x)$$$

Lean4

theorem tendstoUniformly [UniformSpace α] [UniformSpace γ] {f : α → β → γ} (h : UniformContinuous₂ f) :
    TendstoUniformly f (f x) (𝓝 x) :=
  UniformContinuousOn.tendstoUniformly univ_mem <| by rwa [univ_prod_univ, uniformContinuousOn_univ]

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