English
Another articulation of Dini’s theorem on a subset with compactness considerations; monotone F and pointwise convergence imply uniform convergence on the subset.
Русский
Ещё одно оформление теоремы Дини на подмножестве с учётом компактности; монотонная последовательность F и точечное сходение к f дают равномерную сходимость на подмножестве.
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 decreasing collection of continuous functions on a
converging pointwise to a continuous function `f`, then `F n` converges locally uniformly to `f`. -/
theorem tendstoLocallyUniformly_of_forall_tendsto (hF_cont : ∀ i, Continuous (F i)) (hF_anti : Antitone F)
(hf : Continuous f) (h_tendsto : ∀ x, Tendsto (F · x) atTop (𝓝 (f x))) : TendstoLocallyUniformly F f atTop :=
Monotone.tendstoLocallyUniformly_of_forall_tendsto (G := Gᵒᵈ) hF_cont hF_anti hf h_tendsto
