English
Let β be a uniform space. If a family F_i: α → β indexed by ι is uniformly Cauchy on a set s ⊆ α along the atTop filter, and x ∈ s, then the pointwise sequence i ↦ F_i(x) is a Cauchy sequence in β.
Русский
Пусть β - равномерное пространство. Пусть семейство F_i: α → β индексировано ι и равномерно Коши на множестве s ⊆ α по фильтру atTop; тогда для каждого x ∈ s последовательность i ↦ F_i(x) является последовательностью Коши в β.
LaTeX
$$$\\forall x \\in s,\\; \\text{CauchySeq } (i \\mapsto F_i x) $$$
Lean4
/-- If a sequence of functions is uniformly Cauchy on a set, then the values at each point form
a Cauchy sequence. See `UniformCauchySeqOn.cauchy_map` for the non-`atTop` case. -/
theorem cauchySeq [Nonempty ι] [SemilatticeSup ι] (hf : UniformCauchySeqOn F atTop s) (hx : x ∈ s) :
CauchySeq fun i ↦ F i x :=
hf.cauchy_map (hp := atTop_neBot) hx
