English
A two-variable function f: α → β → γ tends uniformly to f(x) near x given a neighborhood U of x and a uniform continuity on U × univ.
Русский
Функция f: α → β → γ стремится равномерно к своему значению в x при приближении к x внутри U.
LaTeX
$$\\text{TendstoUniformlyOn}(f,f(x),U) \\,\\text{for suitable }U \\text{ and } h$$
Lean4
/-- A family of functions `α → β → γ` tends uniformly to its value at `x` if `α` is locally compact,
`β` is compact and `f` is continuous on `U × (univ : Set β)` for some neighborhood `U` of `x`. -/
theorem tendstoUniformly [LocallyCompactSpace α] [CompactSpace β] [UniformSpace γ] {f : α → β → γ} {x : α} {U : Set α}
(hxU : U ∈ 𝓝 x) (h : ContinuousOn ↿f (U ×ˢ univ)) : TendstoUniformly f (f x) (𝓝 x) :=
by
rcases LocallyCompactSpace.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩
have : UniformContinuousOn ↿f (K ×ˢ univ) :=
IsCompact.uniformContinuousOn_of_continuous (hK.prod isCompact_univ) (h.mono <| prod_mono hKU Subset.rfl)
exact this.tendstoUniformly hxK
