α : Type u
β : Type v
X : Type ?u.44437
ι : Type ?u.44440
inst✝ : PseudoMetricSpace α
x y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2
α : Type u
β : Type v
X : Type ?u.44437
ι : Type ?u.44440
inst✝ : PseudoMetricSpace α
x y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε - ε / 2
rw [sub_self_div_two]
no goals
α : Type u
β : Type v
X : Type ?u.44437
ι : Type ?u.44440
inst✝ : PseudoMetricSpace α
x y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2
exact le_of_lt h