subset_ball_lt — Mathlib

English

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

Русский

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

LaTeX

$$∀ h: IsBounded s, ∀ a ∈ ℝ, ∀ c, ∃ r, a < r ∧ s ⊆ ball c r$$

Lean4

theorem _root_.Bornology.IsBounded.subset_ball_lt (h : IsBounded s) (a : ℝ) (c : α) : ∃ r, a < r ∧ s ⊆ ball c r :=
  let ⟨r, hr⟩ := h.subset_closedBall c
  ⟨max r a + 1, (le_max_right _ _).trans_lt (lt_add_one _),
    hr.trans <| closedBall_subset_ball <| (le_max_left _ _).trans_lt (lt_add_one _)⟩

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