closedBall_compl_subset — Mathlib

English

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

Русский

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

LaTeX

$$$IsCobounded\, s \Rightarrow \exists r:\; (closedBall(c,r))^c \subseteq s$$$

Lean4

theorem _root_.Bornology.IsCobounded.closedBall_compl_subset {s : Set α} (hs : IsCobounded s) (c : α) :
    ∃ (r : ℝ), (Metric.closedBall c r)ᶜ ⊆ s :=
  (isCobounded_iff_closedBall_compl_subset c).mp hs

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