Theorems · Theorem · general topology

LipschitzWith.uncurry

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {f : α → β → γ} {Kα Kβ : NNReal},
  (∀ (b : β), LipschitzWith Kα fun a => f a b) →
    (∀ (a : α), LipschitzWith Kβ (f a)) → LipschitzWith (Kα + Kβ) (Function.uncurry f)

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

2 results in Mathlib

Foundations

Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpacePseudoEMetricSpacePseudoEMetricSpace