tendsto_dist_right_cocompact_atTop

English

For a proper space α and fixed x, the function y ↦ dist(y,x) tends to infinity when y tends to infinity (cocompact atTop).

Русский

Для правильного пространства α и фиксированной точки x функция y ↦ dist(y,x) стремится к бесконечности при выходе за пределы любой компактной области.

LaTeX

$$$\operatorname{Tendsto}(\lambda y, \operatorname{dist}(y, x))\; (\operatorname{cocompact}(\alpha))\; \operatorname{atTop}$$$

Lean4

theorem tendsto_dist_right_cocompact_atTop [ProperSpace α] (x : α) : Tendsto (dist · x) (cocompact α) atTop :=
  (tendsto_dist_right_cobounded_atTop x).mono_left cobounded_eq_cocompact.ge

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