∀ {α : Type u_1} {β : Type u_3} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] (G : β → γ) {C : NNReal},
  LipschitzWith C G → ∀ (f : BoundedContinuousFunction α β), Continuous (G ∘ ⇑f)