case intro
α : Type u
β : Type v
X : Type ?u.489346
ι : Type ?u.489349
inst✝ : PseudoMetricSpace α
x : α
s t : Set α
r✝ : ℝ
h : Bounded s
a : ℝ
c : α
r : ℝ
hr : s ⊆ closedBall c r
⊢ ∃ r, a < r ∧ s ⊆ closedBall c r
α : Type u
β : Type v
X : Type ?u.489346
ι : Type ?u.489349
inst✝ : PseudoMetricSpace α
x : α
s t : Set α
r : ℝ
h : Bounded s
a : ℝ
c : α
⊢ ∃ r, a < r ∧ s ⊆ closedBall c r
rcases h.subset_ball c with ⟨r, hr⟩
case intro
α : Type u
β : Type v
X : Type ?u.489346
ι : Type ?u.489349
inst✝ : PseudoMetricSpace α
x : α
s t : Set α
r✝ : ℝ
h : Bounded s
a : ℝ
c : α
r : ℝ
hr : s ⊆ closedBall c r
⊢ s ⊆ closedBall c (max r (a + 1))
case intro
α : Type u
β : Type v
X : Type ?u.489346
ι : Type ?u.489349
inst✝ : PseudoMetricSpace α
x : α
s t : Set α
r✝ : ℝ
h : Bounded s
a : ℝ
c : α
r : ℝ
hr : s ⊆ closedBall c r
⊢ ∃ r, a < r ∧ s ⊆ closedBall c r
refine' ⟨max r (a + 1), lt_of_lt_of_le (by linarith) (le_max_right _ _), _⟩
no goals
case intro
α : Type u
β : Type v
X : Type ?u.489346
ι : Type ?u.489349
inst✝ : PseudoMetricSpace α
x : α
s t : Set α
r✝ : ℝ
h : Bounded s
a : ℝ
c : α
r : ℝ
hr : s ⊆ closedBall c r
⊢ s ⊆ closedBall c (max r (a + 1))
exact hr.trans (closedBall_subset_closedBall (le_max_left _ _))
no goals
α : Type u
β : Type v
X : Type ?u.489346
ι : Type ?u.489349
inst✝ : PseudoMetricSpace α
x : α
s t : Set α
r✝ : ℝ
h : Bounded s
a : ℝ
c : α
r : ℝ
hr : s ⊆ closedBall c r
⊢ a < a + 1
linarith