no goals
α : Type u
β : Type v
X : Type ?u.171036
inst✝² : PseudoEMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → EDist (π b)
f g : (b : β) → π b
d : ℝ≥0∞
⊢ (∀ (b : β), b ∈ Finset.univ → edist (f b) (g b) ≤ d) ↔ ∀ (b : β), edist (f b) (g b) ≤ d
simp only [Finset.mem_univ, forall_const]