English
If F is monotone decreasing, and F x → f x pointwise with f continuous, then F converges locally uniformly to f.
Русский
Если F монотонно убывает и F x → f x по точкам, а f непрерывна, тогда F сходится локально равномерно к f.
LaTeX
$$"Antitone Dini" : (∀ i, Continuous (F i)) → Antitone F → Continuous f → (∀ x, Tendsto (F · x) atTop (𝓝 (f x))) → TendstoLocallyUniformly F f atTop$$
Lean4
/-- **Dini's theorem**: if `F n` is a monotone decreasing collection of continuous functions on a
set `s` converging pointwise to a continuous function `f`, then `F n` converges locally uniformly
to `f`. -/
theorem tendstoLocallyUniformlyOn_of_forall_tendsto {s : Set α} (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))) : TendstoLocallyUniformlyOn F f atTop s :=
Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto (G := Gᵒᵈ) hF_cont hF_anti hf h_tendsto
