comap_dist_left_atTop_eq_cocompact

English

For a proper space α and any x, comap (dist x) atTop equals cocompact α.

Русский

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

LaTeX

$$$\operatorname{comap}(\operatorname{dist} x)\; \operatorname{atTop} = \operatorname{cocompact}(\alpha).$$$

Lean4

theorem comap_dist_left_atTop_eq_cocompact [ProperSpace α] (x : α) : comap (dist x) atTop = cocompact α := by
  simp [cobounded_eq_cocompact]

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