isBounded_iff_subset_closedBall — Mathlib

English

For any c, s is bounded if and only if there exists r with s ⊆ ball(c,r).

Русский

Для каждого центра c существует r такой, что s ⊆ ball(c,r) тогда и только тогда, когда s ограничено.

LaTeX

$$IsBounded(s) ↔ (∃ r, s ⊆ Ball(c,r))$$

Lean4

/-- Given a point, a bounded subset is included in some ball around this point -/
theorem isBounded_iff_subset_closedBall (c : α) : IsBounded s ↔ ∃ r, s ⊆ closedBall c r :=
  ⟨fun h ↦ (isBounded_iff.1 (h.insert c)).imp fun _r hr _x hx ↦ hr (.inr hx) (mem_insert _ _), fun ⟨_r, hr⟩ ↦
    isBounded_closedBall.subset hr⟩

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