V : Type ?u.7597
P : Type u_1
inst✝ : MetricSpace P
p : P
⊢ ∃ radius, ∀ (p_1 : P), p_1 ∈ {p} → dist p_1 p = radius
V : Type ?u.7597
P : Type u_1
inst✝ : MetricSpace P
p : P
⊢ Cospherical {p}
use p
no goals
V : Type ?u.7597
P : Type u_1
inst✝ : MetricSpace P
p : P
⊢ ∃ radius, ∀ (p_1 : P), p_1 ∈ {p} → dist p_1 p = radius
simp