case inl
ι : Sort ?u.97539
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
h : Bounded ∅
⊢ Bounded (thickening δ ∅)

case inr.intro
ι : Sort ?u.97539
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bounded E
x : X
hx : x ∈ E
⊢ Bounded (thickening δ E)
ι : Sort ?u.97539
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bounded E
⊢ Bounded (thickening δ E)
rcases E.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
no goals
case inl
ι : Sort ?u.97539
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
h : Bounded ∅
⊢ Bounded (thickening δ ∅)
simp
case inr.intro
ι : Sort ?u.97539
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ y ∈ closedBall x (δ + diam E)
case inr.intro
ι : Sort ?u.97539
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bounded E
x : X
hx : x ∈ E
⊢ Bounded (thickening δ E)
refine (bounded_iff_subset_ball x).2 ⟨δ + diam E, fun y hy ↦ ?_⟩
no goals
case inr.intro
ι : Sort ?u.97539
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
δ✝ : ℝ
s : Set α
x✝ : α
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ y ∈ closedBall x (δ + diam E)
calc
  dist y x ≤ infDist y E + diam E := dist_le_infDist_add_diam (x := y) h hx
  _ ≤ δ + diam E := add_le_add_right ((mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy).le _