comap_dist_left_atTop — Mathlib

English

For any center c, Tendsto of the distance to c along l to atTop is equivalent to Tendsto f l to cobounded.

Русский

Для каждого центра c предикат Tendsto расстояния до c вдоль фильтра l к atTop эквивалентен Tendsto f l к cobounded.

LaTeX

$$$\operatorname{Tendsto} (\lambda x \mapsto \operatorname{dist}(f x, c))\; l\; \text{atTop} \iff \operatorname{Tendsto} f\; l\; (\operatorname{cobounded}(\alpha))$$$

Lean4

@[simp]
theorem comap_dist_left_atTop (c : α) : comap (dist c) atTop = cobounded α := by
  simpa only [dist_comm _ c] using comap_dist_right_atTop c

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