tendsto_dist_right_atTop_iff — Mathlib

English

For a fixed c, Tendsto of the distance from f x to c to atTop is equivalent to Tendsto f to cobounded.

Русский

Для фиксированного c эквивалентны Tendsto расстояния до c к atTop и Tendsto самой функции к cobounded.

LaTeX

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

Lean4

@[simp]
theorem tendsto_dist_right_atTop_iff (c : α) {f : β → α} {l : Filter β} :
    Tendsto (fun x ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α) := by
  rw [← comap_dist_right_atTop c, tendsto_comap_iff, Function.comp_def]

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