closedBall_compl_subset_of_mem_cocompact

English

If s is cocompact, then there exists r with (closedBall c r)^c ⊆ s for any center c.

Русский

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

LaTeX

$$$Filter.instMembership.mem (Filter.cocompact(\alpha)) s \Rightarrow \exists r:\; (closedBall(c,r))^c \subseteq s$$$

Lean4

theorem closedBall_compl_subset_of_mem_cocompact {s : Set α} (hs : s ∈ cocompact α) (c : α) :
    ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s :=
  IsCobounded.closedBall_compl_subset (cobounded_le_cocompact hs) c

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