subset_closedBall_lt — Mathlib

English

If s is bounded, then for any a ∈ ℝ and center c there exists r with a < r and s ⊆ closedBall(c,r).

Русский

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

LaTeX

$$IsBounded(s) → ∀ c, ∃ r, a < r ∧ s ⊆ closedBall c r$$

Lean4

theorem _root_.Bornology.IsBounded.subset_closedBall_lt (h : IsBounded s) (a : ℝ) (c : α) :
    ∃ r, a < r ∧ s ⊆ closedBall c r :=
  let ⟨r, har, hr⟩ := h.subset_ball_lt a c
  ⟨r, har, hr.trans ball_subset_closedBall⟩

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