case pos
α : Type u
β : Type v
X : Type ?u.395267
ι : Type ?u.395270
inst✝³ : PseudoMetricSpace α
π : β → Type u_1
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

case neg
α : Type u
β : Type v
X : Type ?u.395267
ι : Type ?u.395270
inst✝³ : PseudoMetricSpace α
π : β → Type u_1
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
hr : ¬0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
α : Type u
β : Type v
X : Type ?u.395267
ι : Type ?u.395270
inst✝³ : PseudoMetricSpace α
π : β → Type u_1
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
by_cases hr : 0 ≤ r
no goals
case pos
α : Type u
β : Type v
X : Type ?u.395267
ι : Type ?u.395270
inst✝³ : PseudoMetricSpace α
π : β → Type u_1
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
exact dist_pi_le_iff hr
no goals
case neg
α : Type u
β : Type v
X : Type ?u.395267
ι : Type ?u.395270
inst✝³ : PseudoMetricSpace α
π : β → Type u_1
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
hr : ¬0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
exact iff_of_false (fun h => hr <| dist_nonneg.trans h) fun h =>
  hr <| dist_nonneg.trans <| h <| Classical.arbitrary _