English
On a compact set s, if F i are continuous on s, F is monotone on s and F x → f x, then F →f uniformly on s.
Русский
На компактном множестве s, если F_i непрерывны на s, F монотонна на s и F x → f x, то F сходится к 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 space converging pointwise to a continuous function `f`, then `F n` converges uniformly to
`f`. -/
theorem tendstoUniformly_of_forall_tendsto [CompactSpace α] (hF_cont : ∀ i, Continuous (F i)) (hF_mono : Monotone F)
(hf : Continuous f) (h_tendsto : ∀ x, Tendsto (F · x) atTop (𝓝 (f x))) : TendstoUniformly F f atTop :=
tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace.mp <|
tendstoLocallyUniformly_of_forall_tendsto hF_cont hF_mono hf h_tendsto
