tendsto_cocompact_of_tendsto_dist_comp_atTop

English

If f is a map β → α and the distance to a fixed x converges to infinity along l, then f tends to cocompact along l.

Русский

Если функция f:β→α такова, что dist(f(y), x) → ∞ по мере движения y по фильтру l, то f l расходится к коккомпактному фильтру.

LaTeX

$$$\text{If } h : \operatorname{Tendsto}(\lambda y, \operatorname{dist}(f(y), x)) l \operatorname{atTop}, \text{ then } \operatorname{Tendsto} f l \operatorname{cocompact}.$$$

Lean4

theorem tendsto_cocompact_of_tendsto_dist_comp_atTop {f : β → α} {l : Filter β} (x : α)
    (h : Tendsto (fun y => dist (f y) x) l atTop) : Tendsto f l (cocompact α) :=
  ((tendsto_dist_right_atTop_iff _).1 h).mono_right cobounded_le_cocompact

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