English
If F is monotone increasing, F continuous, f continuous and F converges pointwise to f, then F converges uniformly to f.
Русский
Если F монотонно возрастает и сходится точечно к f, а f непрерывна, то F сходится равномерно к f.
LaTeX
$$"Dini's theorem" : (∀ i, Continuous (F i)) → Monotone F → Continuous f → (∀ x, Tendsto (F · x) atTop (𝓝 (f x))) → TendstoUniformly F f atTop$$
Lean4
/-- **Dini's theorem**: if `F n` is a monotone increasing 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_mono : ∀ x ∈ s, Monotone (F · x)) (hf : ContinuousOn f s)
(h_tendsto : ∀ x ∈ s, Tendsto (F · x) atTop (𝓝 (f x))) : TendstoLocallyUniformlyOn F f atTop s :=
by
rw [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe]
exact
tendstoLocallyUniformly_of_forall_tendsto (hF_cont · |>.restrict) (fun _ _ h x ↦ hF_mono _ x.2 h) hf.restrict
(fun x ↦ h_tendsto x x.2)
