tendsto_dist_left_cocompact_atTop

English

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

Русский

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

LaTeX

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

Lean4

theorem tendsto_dist_left_cocompact_atTop [ProperSpace α] (x : α) : Tendsto (dist x) (cocompact α) atTop :=
  (tendsto_dist_left_cobounded_atTop x).mono_left cobounded_eq_cocompact.ge

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