Theorems · Theorem · general topology

LipschitzOnWith.ediam_image2_le

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α → β → γ) {K₁ K₂ : NNReal} (s : Set α) (t : Set β),
  (∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s) →
    (∀ a ∈ s, LipschitzOnWith K₂ (f a) t) →
      Metric.ediam (Set.image2 f s t) ≤ ↑K₁ * Metric.ediam s + ↑K₂ * Metric.ediam t

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpacePseudoEMetricSpace