isCobounded_iff_closedBall_compl_subset

English

IsCobounded s iff there exists centers c and radius r such that (closedBall c r)^c ⊆ s.

Русский

IsCobounded s эквивалентно существованию центра c и радиуса r с (closedBall c r)^c ⊆ s.

LaTeX

$$$IsCobounded\, s \iff \exists c\in\alpha, \exists r\in\mathbb{R}, (closedBall(c,r))^c \subseteq s$$$

Lean4

theorem isCobounded_iff_closedBall_compl_subset {s : Set α} (c : α) :
    IsCobounded s ↔ ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s :=
  by
  rw [← isBounded_compl_iff, isBounded_iff_subset_closedBall c]
  apply exists_congr
  intro r
  rw [compl_subset_comm]

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