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 _)⟩