English
A variant of Dini’s theorem for uniform convergence on a subset; if monotone conditions hold on s and convergence pointwise to f with f continuous on s, then uniform convergence on s follows.
Русский
Вариация теоремы Дини для равномерной свёртки на подмножестве; при монотонности и сходящемся точечно к непрерывной на s функции f, получаем равномерную сходимость на s.
LaTeX
$$IsCompact s → (∀ i, ContinuousOn (F i) s) → (∀ x ∈ s, Monotone (F · x)) → (ContinuousOn f s) → (∀ x ∈ s, Tendsto (F · x) atTop (𝓝 (f x))) → TendstoUniformlyOn F f atTop s$$
Lean4
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions on a
compact set `s` converging pointwise to a continuous function `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_mono : ∀ x ∈ s, Monotone (F · x)) (hf : ContinuousOn f s)
(h_tendsto : ∀ x ∈ s, Tendsto (F · x) atTop (𝓝 (f x))) : TendstoUniformlyOn F f atTop s :=
tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hs |>.mp <|
tendstoLocallyUniformlyOn_of_forall_tendsto hF_cont hF_mono hf h_tendsto
