case inl
α : Type u
β : Type v
X : Type ?u.552898
ι : Type ?u.552901
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝ : γ
s : Set γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ Set.Subsingleton (closedBall x r)

case inr
α : Type u
β : Type v
X : Type ?u.552898
ι : Type ?u.552901
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝ : γ
s : Set γ
x : γ
hr : 0 ≤ 0
⊢ Set.Subsingleton (closedBall x 0)
α : Type u
β : Type v
X : Type ?u.552898
ι : Type ?u.552901
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝ : γ
s : Set γ
x : γ
r : ℝ
hr : r ≤ 0
⊢ Set.Subsingleton (closedBall x r)
rcases hr.lt_or_eq with (hr | rfl)
case inl
α : Type u
β : Type v
X : Type ?u.552898
ι : Type ?u.552901
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝ : γ
s : Set γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ Set.Subsingleton ∅
case inl
α : Type u
β : Type v
X : Type ?u.552898
ι : Type ?u.552901
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝ : γ
s : Set γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ Set.Subsingleton (closedBall x r)
rw [closedBall_eq_empty.2 hr]
no goals
case inl
α : Type u
β : Type v
X : Type ?u.552898
ι : Type ?u.552901
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝ : γ
s : Set γ
x : γ
r : ℝ
hr✝ : r ≤ 0
hr : r < 0
⊢ Set.Subsingleton ∅
exact subsingleton_empty
case inr
α : Type u
β : Type v
X : Type ?u.552898
ι : Type ?u.552901
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝ : γ
s : Set γ
x : γ
hr : 0 ≤ 0
⊢ Set.Subsingleton {x}
case inr
α : Type u
β : Type v
X : Type ?u.552898
ι : Type ?u.552901
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝ : γ
s : Set γ
x : γ
hr : 0 ≤ 0
⊢ Set.Subsingleton (closedBall x 0)
rw [closedBall_zero]
no goals
case inr
α : Type u
β : Type v
X : Type ?u.552898
ι : Type ?u.552901
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x✝ : γ
s : Set γ
x : γ
hr : 0 ≤ 0
⊢ Set.Subsingleton {x}
exact subsingleton_singleton