ι : Sort ?u.158407
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x✝ : α
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ x ∈ cthickening ε (cthickening δ s) → x ∈ cthickening (ε + δ) s
ι : Sort ?u.158407
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x : α
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
⊢ cthickening ε (cthickening δ s) ⊆ cthickening (ε + δ) s
intro x
ι : Sort ?u.158407
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x✝ : α
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEdist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
ι : Sort ?u.158407
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x✝ : α
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ x ∈ cthickening ε (cthickening δ s) → x ∈ cthickening (ε + δ) s
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]
no goals
ι : Sort ?u.158407
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s✝ t : Set α
x✝ : α
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEdist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
exact fun hx => infEdist_le_infEdist_cthickening_add.trans (add_le_add_right hx _)