English
A family of pairs f:ι→α×α tends to the uniformity iff the distance between the two coordinates tends to 0.
Русский
Степень сходимости пары точек к униформности равна тому, что расстояние между компонентами сходится к нулю.
LaTeX
$$$\operatorname{Tendsto} f\, p\, \mathcal U(\alpha) \;\Longleftrightarrow\; \operatorname{Tendsto} \bigl(\lambda x. \operatorname{dist}(f x)_1(f x)_2\bigr) p\, \mathcal N(0)$$$
Lean4
theorem tendsto_uniformity_iff_dist_tendsto_zero {f : ι → α × α} {p : Filter ι} :
Tendsto f p (𝓤 α) ↔ Tendsto (fun x => dist (f x).1 (f x).2) p (𝓝 0) := by
rw [Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff, Function.comp_def]