cobounded_eq_cocompact — Mathlib

English

In a proper space, the cobounded filter equals the cocompact filter.

Русский

В правильном пространстве кобундированное фильтр совпадает с кокомпактным фильтром.

LaTeX

$$$\operatorname{cobounded}(\alpha) = \operatorname{cocompact}(\alpha).$$$

Lean4

theorem cobounded_eq_cocompact [ProperSpace α] : cobounded α = cocompact α :=
  by
  nontriviality α; inhabit α
  exact
    cobounded_le_cocompact.antisymm <|
      (hasBasis_cobounded_compl_closedBall default).ge_iff.2 fun _ _ ↦ (isCompact_closedBall _ _).compl_mem_cocompact

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