α : Type u
β : Type v
X : Type ?u.43836
ι : Type ?u.43839
inst✝ : PseudoMetricSpace α
x y z✝ : α
δ ε ε₁ ε₂ : ℝ
s : Set α
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y (ε₁ + (ε₂ - ε₁))
α : Type u
β : Type v
X : Type ?u.43836
ι : Type ?u.43839
inst✝ : PseudoMetricSpace α
x y z✝ : α
δ ε ε₁ ε₂ : ℝ
s : Set α
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y ε₂
rw [← add_sub_cancel'_right ε₁ ε₂]
no goals
α : Type u
β : Type v
X : Type ?u.43836
ι : Type ?u.43839
inst✝ : PseudoMetricSpace α
x y z✝ : α
δ ε ε₁ ε₂ : ℝ
s : Set α
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y (ε₁ + (ε₂ - ε₁))
exact lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h)