English
If F is an antitone (decreasing) family of continuous maps F_i: α → G converging pointwise to f, then F → 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 (Antitone 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 decreasing 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_antitone_of_pointwise (hF_anti : Antitone F) (h_tendsto : ∀ x, Tendsto (F · x) atTop (𝓝 (f x))) :
Tendsto F atTop (𝓝 f) :=
tendsto_of_monotone_of_pointwise (G := Gᵒᵈ) hF_anti h_tendsto
