English
If U is a neighborhood of x in α, and F is a uniformly continuous-on-U function with values in β, then F behaves uniformly near x; i.e., TendstoUniformly F (F x) (nhds x) holds when restricted to the neighborhood U.
Русский
Если F непрерывна равномерно на окрестности U и значения в β, то сходится равномерно в окрестности x.
LaTeX
$$TendstoUniformly F (F x) (nhds x)$$
Lean4
theorem tendstoUniformlyOn [UniformSpace α] [UniformSpace γ] {U : Set α} {V : Set β} {F : α → β → γ}
(hF : UniformContinuousOn ↿F (U ×ˢ V)) (hU : x ∈ U) : TendstoUniformlyOn F (F x) (𝓝[U] x) V :=
by
set φ := fun q : α × β => ((x, q.2), q)
rw [tendstoUniformlyOn_iff_tendsto]
change Tendsto (Prod.map ↿F ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
simp only [nhdsWithin, Filter.prod_eq_inf, comap_inf, inf_assoc, comap_principal, inf_principal]
refine hF.comp (Tendsto.inf ?_ <| tendsto_principal_principal.2 fun x hx => ⟨⟨hU, hx.2⟩, hx⟩)
simp only [uniformity_prod_eq_comap_prod, tendsto_comap_iff, nhds_eq_comap_uniformity, comap_comap]
exact tendsto_comap.prodMk (tendsto_diag_uniformity _ _)
