α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ
⊢ LipschitzWith (1 + 1) (uncurry dist)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ
⊢ LipschitzWith 2 (uncurry dist)
rw [← one_add_one_eq_two]
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ
⊢ LipschitzWith (1 + 1) (uncurry dist)
exact LipschitzWith.uncurry LipschitzWith.dist_left LipschitzWith.dist_right