mem_cocompact_of_closedBall_compl_subset

English

If there exists r with (closedBall c r)^c ⊆ s, then s is cocompact (under proper space).

Русский

Если существует r такое, что (closedBall c r)^c ⊆ s, то s принадлежит cocompact (при допустимом пространстве).

LaTeX

$$$\exists r:\; (closedBall(c,r))^c \subseteq s \Rightarrow s \in cocompact(\alpha)$$$

Lean4

theorem mem_cocompact_of_closedBall_compl_subset [ProperSpace α] (c : α) (h : ∃ r, (closedBall c r)ᶜ ⊆ s) :
    s ∈ cocompact α := by
  rcases h with ⟨r, h⟩
  rw [Filter.mem_cocompact]
  exact ⟨closedBall c r, isCompact_closedBall c r, h⟩

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