α : Type u
β : Type v
X : Type ?u.239698
ι : Type ?u.239701
inst✝ : PseudoMetricSpace α
z : ℝ≥0
⊢ nndist 0 z = z
α : Type u
β : Type v
X : Type ?u.239698
ι : Type ?u.239701
inst✝ : PseudoMetricSpace α
z : ℝ≥0
⊢ nndist z 0 = z
rw [nndist_comm]
no goals
α : Type u
β : Type v
X : Type ?u.239698
ι : Type ?u.239701
inst✝ : PseudoMetricSpace α
z : ℝ≥0
⊢ nndist 0 z = z
exact NNReal.nndist_zero_eq_val z