tendsto_uniformity_iff_dist_tendsto_zero

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]

Похожие утверждения