English
Let x ∈ closure S. If F is equicontinuous at x and f converges to z along nhdsWithin x S, and if for all y ∈ S, F(·, y) tends to f(y) along l, then F(·, x) tends to z along l.
Русский
Пусть x лежит в closure S. Если F эконтинуальна в x, f сходится к z вдоль nhdsWithin x S, и для каждого y ∈ S F(·, y) сходится к f(y) вдоль l, тогда F(·, x) сходится к z вдоль l.
LaTeX
$$$\text{EquicontinuousAt } F x \land \text{Tendsto } f (\mathcal{N}[S] x) z \land \forall y\in S, Tendsto (F·y) l (\mathcal{N}(f y)) \land x\in\overline{S} \Rightarrow Tendsto (F·x) l (\mathcal{N} z)$$$
Lean4
/-- If `𝓕 : ι → β → α` tends to `f : β → α` *pointwise* along some nontrivial filter, and if the
family `𝓕` is uniformly equicontinuous, then the limit is uniformly continuous. -/
theorem uniformContinuous_of_uniformEquicontinuous {l : Filter ι} [l.NeBot] {F : ι → β → α} {f : β → α}
(h₁ : Tendsto F l (𝓝 f)) (h₂ : UniformEquicontinuous F) : UniformContinuous f :=
by
rw [← uniformContinuousOn_univ, ← uniformEquicontinuousOn_univ, tendsto_pi_nhds] at *
exact uniformContinuousOn_of_uniformEquicontinuousOn (fun x _ ↦ h₁ x) h₂
