English
Let F : ι → α → β and f : α → β. Then F tends to f locally uniformly on s with respect to p if and only if for every x in s, the map (i, y) ↦ (f(y), F(i, y)) tends to the diagonal in β along the product filter p × 𝓝[s] x.
Русский
Пусть F : ι → α → β и f : α → β. Тогда F сходится локально равномерно к f на s по фильтру p тогда и только тогда, когда для каждого x ∈ s отображение (i, y) ↦ (f(y), F(i, y)) сходится к диагонали в β по фильтру произведения p × 𝓝[s] x.
LaTeX
$$$$\operatorname{TendstoLocallyUniformlyOn}(F,f,p,s) \iff \forall x\in s,\ \operatorname{Tendsto}\Bigl((i,y) \mapsto (f(y), F(i,y))\Bigr)\bigl(p \times\mathcal{N}_{s}(x)\bigr) \bigl(\mathcal{U}(\beta)\bigr).$$$$
Lean4
theorem tendstoLocallyUniformlyOn_iff_forall_tendsto :
TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β) :=
forall₂_swap.trans <| forall₄_congr fun _ _ _ _ => by simp_rw [mem_map, mem_prod_iff_right, mem_preimage]
