English
Let s be a compact subset of α. If F_i: α → G are continuous on s (ContinuousOn) and decrease with i on s (Antitone (F · x) for x ∈ s), and f is continuous on s with pointwise convergence to f on s, then F_i → f uniformly on s.
Русский
Пусть s ⊂ α компактно. Пусть F_i: α → G непрерывны на s и уменьшаются по i на s, а f непрерывна на s и F_i(x) сходится к f(x) для каждого x ∈ s. Тогда F_i → f равномерно на s.
LaTeX
$$$[\text{IsCompact } s] \Rightarrow (\forall i, F_i \text{ continuousOn } s) \land (\forall x \in s, Antitone (F · x)) \land (f \text{ continuousOn } s) \land (\forall x \in s, Tendsto (F · x) atTop (nhds (f x))) \Rightarrow \ TendstoUniformlyOn F f atTop s$$$
Lean4
/-- **Dini's theorem**: if `F n` is a monotone decreasing collection of continuous functions on a
compact set `s` converging pointwise to a continuous `f`, then `F n` converges uniformly to `f`. -/
theorem tendstoUniformlyOn_of_forall_tendsto {s : Set α} (hs : IsCompact s) (hF_cont : ∀ i, ContinuousOn (F i) s)
(hF_anti : ∀ x ∈ s, Antitone (F · x)) (hf : ContinuousOn f s)
(h_tendsto : ∀ x ∈ s, Tendsto (F · x) atTop (𝓝 (f x))) : TendstoUniformlyOn F f atTop s :=
Monotone.tendstoUniformlyOn_of_forall_tendsto (G := Gᵒᵈ) hs hF_cont hF_anti hf h_tendsto
