α : Type u
β : Type v
X : Type ?u.397955
ι : Type ?u.397958
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
b : β
⊢ edist (f b) (g b) ≤ edist f g
α : Type u
β : Type v
X : Type ?u.397955
ι : Type ?u.397958
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
b : β
⊢ nndist (f b) (g b) ≤ nndist f g
rw [← ENNReal.coe_le_coe, ← edist_nndist, ← edist_nndist]
no goals
α : Type u
β : Type v
X : Type ?u.397955
ι : Type ?u.397958
inst✝² : PseudoMetricSpace α
π : β → Type u_1
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
b : β
⊢ edist (f b) (g b) ≤ edist f g
exact edist_le_pi_edist f g b