case h
α : Type u
β : Type v
X : Type ?u.164899
ι : Type ?u.164902
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
y : α
⊢ y ∈ EMetric.closedBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε
α : Type u
β : Type v
X : Type ?u.164899
ι : Type ?u.164902
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
⊢ EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε
ext y
no goals
case h
α : Type u
β : Type v
X : Type ?u.164899
ι : Type ?u.164902
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
y : α
⊢ y ∈ EMetric.closedBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε
simp [edist_le_ofReal h]