English
Let α be a compact space and G be a normed, lattice-ordered additive group with a solid norm. If (F_i) is a family of continuous functions F_i: α → G that decreases with i (antitone in i) and converges pointwise to a continuous function f: α → G, then F_i converges uniformly to f on α.
Русский
Пусть α — компактное множество и G — нормированная решеточная аддитивная группа с твердой нормой. Если семейство функций F_i: α → G монотонно не возрастает по i (антиодично по i) и сходится по каждой точке к непрерывной функции f: α → G, то F_i сходится равномерно к f на α.
LaTeX
$$$[\text{CompactSpace }\alpha] \Rightarrow (\forall i, F_i \in C(\alpha,G)) \,\land\, (Antitone F) \,\land\ (f \in C(\alpha,G)) \,\land\ (\forall x \in \alpha, \ Tendsto (F_i(x))_{i\to\infty} (nhds (f(x)))) \Rightarrow \ TendstoUniformly F f \ atTop$$$
Lean4
/-- **Dini's theorem**: if `F n` is a monotone decreasing 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_anti : Antitone F)
(hf : Continuous f) (h_tendsto : ∀ x, Tendsto (F · x) atTop (𝓝 (f x))) : TendstoUniformly F f atTop :=
Monotone.tendstoUniformly_of_forall_tendsto (G := Gᵒᵈ) hF_cont hF_anti hf h_tendsto
