case intro
α : Type u
β : Type v
X : Type ?u.394814
ι : Type ?u.394817
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
⊢ dist f g ≤ ↑r ↔ ∀ (b : β), dist (f b) (g b) ≤ ↑r
α : Type u
β : Type v
X : Type ?u.394814
ι : Type ?u.394817
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
lift r to ℝ≥0 using hr
no goals
case intro
α : Type u
β : Type v
X : Type ?u.394814
ι : Type ?u.394817
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
⊢ dist f g ≤ ↑r ↔ ∀ (b : β), dist (f b) (g b) ≤ ↑r
exact nndist_pi_le_iff