∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] [inst_1 : PseudoEMetricSpace β]
  {f : γ → α → β} {K : NNReal},
  (LipschitzWith K fun x => UniformFun.ofFun (f x)) ↔ ∀ (c : α), LipschitzWith K fun x => f x c