English
If F is a monotone increasing family of continuous maps F_i: α → G converging pointwise to a continuous f, then F converges to f in the compact-open topology.
Русский
Если F — монотонное возрастающее семейство непрерывных отображений F_i: α → G, сходящееся по каждой точке к непрерывной f, то F сходится к f в компактно-открытой топологии.
LaTeX
$$$[\text{CompactSpace }\alpha] \Rightarrow (\forall i, F_i \in C(\alpha,G)) \land (Monotone F) \land (f \in C(\alpha,G)) \land (\forall x, Tendsto (F · x) atTop (nhds (f x))) \Rightarrow Tendsto F atTop (nhds f)$$$
Lean4
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions
converging pointwise to a continuous function `f`, then `F n` converges to `f` in the
compact-open topology. -/
theorem tendsto_of_monotone_of_pointwise (hF_mono : Monotone F) (h_tendsto : ∀ x, Tendsto (F · x) atTop (𝓝 (f x))) :
Tendsto F atTop (𝓝 f) :=
tendsto_of_tendstoLocallyUniformly <|
hF_mono.tendstoLocallyUniformly_of_forall_tendsto (F · |>.continuous) f.continuous h_tendsto
