α : Type u
β : Type v
X : Type ?u.164621
ι : Type ?u.164624
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ EMetric.ball x ↑ε = EMetric.ball x (ENNReal.ofReal ↑ε)
α : Type u
β : Type v
X : Type ?u.164621
ι : Type ?u.164624
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ EMetric.ball x ↑ε = ball x ↑ε
rw [← Metric.emetric_ball]
no goals
α : Type u
β : Type v
X : Type ?u.164621
ι : Type ?u.164624
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ EMetric.ball x ↑ε = EMetric.ball x (ENNReal.ofReal ↑ε)
simp