case h
α : Type u
β : Type v
X : Type ?u.164248
ι : Type ?u.164251
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ EMetric.ball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε
α : Type u
β : Type v
X : Type ?u.164248
ι : Type ?u.164251
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ EMetric.ball x (ENNReal.ofReal ε) = ball x ε
ext y
case h
α : Type u
β : Type v
X : Type ?u.164248
ι : Type ?u.164251
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε
case h
α : Type u
β : Type v
X : Type ?u.164248
ι : Type ?u.164251
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ EMetric.ball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε
simp only [EMetric.mem_ball, mem_ball, edist_dist]
no goals
case h
α : Type u
β : Type v
X : Type ?u.164248
ι : Type ?u.164251
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε
exact ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg