α : Type u
β : Type v
X : Type ?u.33233
ι : Type ?u.33236
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝ : Subsingleton α
hε : ε ≠ 0
⊢ IsEmpty ↑∅
α : Type u
β : Type v
X : Type ?u.33233
ι : Type ?u.33236
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝ : Subsingleton α
hε : ε ≠ 0
⊢ IsEmpty ↑(sphere x ε)
rw [sphere_eq_empty_of_subsingleton hε]
no goals
α : Type u
β : Type v
X : Type ?u.33233
ι : Type ?u.33236
inst✝¹ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝ : Subsingleton α
hε : ε ≠ 0
⊢ IsEmpty ↑∅
infer_instance