no goals
α : Type u
β : Type v
X : Type ?u.389587
ι : Type ?u.389590
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
⊢ nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r
simp [nndist_pi_def]