tendsto_dist_left_atTop_iff — Mathlib

English

For center c, Tendsto of dist c (f x) to atTop is equivalent to Tendsto f to cobounded.

Русский

Для центра c сходность расстояния от c к f x к бесконечности эквивалентна тому, что f стремится к cobounded.

LaTeX

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

Lean4

@[simp]
theorem tendsto_dist_left_atTop_iff (c : α) {f : β → α} {l : Filter β} :
    Tendsto (fun x ↦ dist c (f x)) l atTop ↔ Tendsto f l (cobounded α) := by
  simp only [dist_comm c, tendsto_dist_right_atTop_iff]

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