Documentation

Mathlib.Topology.EMetricSpace.Lipschitz

Lipschitz continuous functions #

A map f : α → β between two (extended) metric spaces is called Lipschitz continuous with constant K ≥ 0 if for all x, y we have edist (f x) (f y) ≤ K * edist x y. For a metric space, the latter inequality is equivalent to dist (f x) (f y) ≤ K * dist x y. There is also a version asserting this inequality only for x and y in some set s. Finally, f : α → β is called locally Lipschitz continuous if each x : α has a neighbourhood on which f is Lipschitz continuous (with some constant).

In this file we provide various ways to prove that various combinations of Lipschitz continuous functions are Lipschitz continuous. We also prove that Lipschitz continuous functions are uniformly continuous, and that locally Lipschitz functions are continuous.

Main definitions and lemmas #

LipschitzWith K f: states that f is Lipschitz with constant K : ℝ≥0
LipschitzOnWith K f s: states that f is Lipschitz with constant K : ℝ≥0 on a set s
LipschitzWith.uniformContinuous: a Lipschitz function is uniformly continuous
LipschitzOnWith.uniformContinuousOn: a function which is Lipschitz on a set s is uniformly continuous on s.
LocallyLipschitz f: states that f is locally Lipschitz
LocallyLipschitz.continuous: a locally Lipschitz function is continuous.

Implementation notes #

The parameter K has type ℝ≥0. This way we avoid conjunction in the definition and have coercions both to ℝ and ℝ≥0∞. Constructors whose names end with ' take K : ℝ as an argument, and return LipschitzWith (Real.toNNReal K) f.

def LipschitzWith {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) :

A function f is Lipschitz continuous with constant K ≥ 0 if for all x, y we have dist (f x) (f y) ≤ K * dist x y.

Equations

LipschitzWith K f = ∀ (x y : α), edist (f x) (f y) ≤ ↑K * edist x y

Instances For

def LipschitzOnWith {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) (s : Set α) :

A function f is Lipschitz continuous with constant K ≥ 0 on s if for all x, y in s we have dist (f x) (f y) ≤ K * dist x y.

Equations

LipschitzOnWith K f s = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → edist (f x) (f y) ≤ ↑K * edist x y

Instances For

def LocallyLipschitz {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) :

f : α → β is called locally Lipschitz continuous iff every point x has a neighourhood on which f is Lipschitz.

Equations

LocallyLipschitz f = ∀ (x : α), ∃ (K : NNReal), ∃ t ∈ nhds x, LipschitzOnWith K f t

Instances For

@[simp]

theorem lipschitzOnWith_empty {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) :

LipschitzOnWith K f ∅

Every function is Lipschitz on the empty set (with any Lipschitz constant).

theorem LipschitzOnWith.mono {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {t : Set α} {f : α → β} (hf : LipschitzOnWith K f t) (h : s ⊆ t) :

LipschitzOnWith K f s

Being Lipschitz on a set is monotone w.r.t. that set.

@[simp]

theorem lipschitzOn_univ {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} :

LipschitzOnWith K f Set.univ ↔ LipschitzWith K f

f is Lipschitz iff it is Lipschitz on the entire space.

theorem lipschitzOnWith_iff_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {s : Set α} :

LipschitzOnWith K f s ↔ LipschitzWith K (Set.restrict s f)

theorem LipschitzOnWith.to_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {s : Set α} :

LipschitzOnWith K f s → LipschitzWith K (Set.restrict s f)

Alias of the forward direction of lipschitzOnWith_iff_restrict.

theorem MapsTo.lipschitzOnWith_iff_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) :

LipschitzOnWith K f s ↔ LipschitzWith K (Set.MapsTo.restrict f s t h)

theorem LipschitzOnWith.to_restrict_mapsTo {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) :

LipschitzOnWith K f s → LipschitzWith K (Set.MapsTo.restrict f s t h)

Alias of the forward direction of MapsTo.lipschitzOnWith_iff_restrict.

theorem LipschitzWith.lipschitzOnWith {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (s : Set α) :

LipschitzOnWith K f s

theorem LipschitzWith.edist_le_mul {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (x : α) (y : α) :

edist (f x) (f y) ≤ ↑K * edist x y

theorem LipschitzWith.edist_le_mul_of_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {x : α} {y : α} {r : ENNReal} (h : LipschitzWith K f) (hr : edist x y ≤ r) :

edist (f x) (f y) ≤ ↑K * r

theorem LipschitzWith.edist_lt_mul_of_lt {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {x : α} {y : α} {r : ENNReal} (h : LipschitzWith K f) (hK : K ≠ 0) (hr : edist x y < r) :

edist (f x) (f y) < ↑K * r

theorem LipschitzWith.mapsTo_emetric_closedBall {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (x : α) (r : ENNReal) :

Set.MapsTo f (EMetric.closedBall x r) (EMetric.closedBall (f x) (↑K * r))

theorem LipschitzWith.mapsTo_emetric_ball {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (hK : K ≠ 0) (x : α) (r : ENNReal) :

Set.MapsTo f (EMetric.ball x r) (EMetric.ball (f x) (↑K * r))

theorem LipschitzWith.edist_lt_top {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {x : α} {y : α} (h : edist x y ≠ ⊤) :

edist (f x) (f y) < ⊤

theorem LipschitzWith.mul_edist_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (x : α) (y : α) :

(↑K)⁻¹ * edist (f x) (f y) ≤ edist x y

theorem LipschitzWith.of_edist_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : ∀ (x y : α), edist (f x) (f y) ≤ edist x y) :

LipschitzWith 1 f

theorem LipschitzWith.weaken {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {K' : NNReal} (h : K ≤ K') :

LipschitzWith K' f

theorem LipschitzWith.ediam_image_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (s : Set α) :

EMetric.diam (f '' s) ≤ ↑K * EMetric.diam s

theorem LipschitzWith.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {x : α} {y : α} {d : ENNReal} (h : edist x y < d / ↑K) :

edist (f x) (f y) < d

theorem LipschitzWith.uniformContinuous {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) :

UniformContinuous f

A Lipschitz function is uniformly continuous.

theorem LipschitzWith.continuous {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) :

A Lipschitz function is continuous.

theorem LipschitzWith.const {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) :

LipschitzWith 0 fun (x : α) => b

Constant functions are Lipschitz (with any constant).

theorem LipschitzWith.const' {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) {K : NNReal} :

LipschitzWith K fun (x : α) => b

theorem LipschitzWith.id {α : Type u} [PseudoEMetricSpace α] :

LipschitzWith 1 id

The identity is 1-Lipschitz.

theorem LipschitzWith.subtype_val {α : Type u} [PseudoEMetricSpace α] (s : Set α) :

LipschitzWith 1 Subtype.val

The inclusion of a subset is 1-Lipschitz.

theorem LipschitzWith.subtype_mk {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {p : β → Prop} (hp : ∀ (x : α), p (f x)) :

LipschitzWith K fun (x : α) => { val := f x, property := (_ : p (f x)) }

theorem LipschitzWith.eval {ι : Type x} {α : ι → Type u} [(i : ι) → PseudoEMetricSpace (α i)] [Fintype ι] (i : ι) :

LipschitzWith 1 (Function.eval i)

theorem LipschitzWith.restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (s : Set α) :

LipschitzWith K (Set.restrict s f)

The restriction of a K-Lipschitz function is K-Lipschitz.

theorem LipschitzWith.comp {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {Kf : NNReal} {Kg : NNReal} {f : β → γ} {g : α → β} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :

LipschitzWith (Kf * Kg) (f ∘ g)

The composition of Lipschitz functions is Lipschitz.

theorem LipschitzWith.comp_lipschitzOnWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {Kf : NNReal} {Kg : NNReal} {f : β → γ} {g : α → β} {s : Set α} (hf : LipschitzWith Kf f) (hg : LipschitzOnWith Kg g s) :

LipschitzOnWith (Kf * Kg) (f ∘ g) s

theorem LipschitzWith.prod_fst {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] :

LipschitzWith 1 Prod.fst

theorem LipschitzWith.prod_snd {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] :

LipschitzWith 1 Prod.snd

theorem LipschitzWith.prod {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : α → β} {Kf : NNReal} (hf : LipschitzWith Kf f) {g : α → γ} {Kg : NNReal} (hg : LipschitzWith Kg g) :

LipschitzWith (max Kf Kg) fun (x : α) => (f x, g x)

If f and g are Lipschitz functions, so is the induced map f × g to the product type.

theorem LipschitzWith.prod_mk_left {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (a : α) :

LipschitzWith 1 (Prod.mk a)

theorem LipschitzWith.prod_mk_right {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) :

LipschitzWith 1 fun (a : α) => (a, b)

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

LipschitzWith (Kα + Kβ) (Function.uncurry f)

theorem LipschitzWith.iterate {α : Type u} [PseudoEMetricSpace α] {K : NNReal} {f : α → α} (hf : LipschitzWith K f) (n : ℕ) :

LipschitzWith (K ^ n) f^[n]

Iterates of a Lipschitz function are Lipschitz.

theorem LipschitzWith.edist_iterate_succ_le_geometric {α : Type u} [PseudoEMetricSpace α] {K : NNReal} {f : α → α} (hf : LipschitzWith K f) (x : α) (n : ℕ) :

edist (f ^[n] x) (f ^[n + 1] x) ≤ edist x (f x) * ↑K ^ n

theorem LipschitzWith.mul_end {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} {g : Function.End α} {Kf : NNReal} {Kg : NNReal} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :

LipschitzWith (Kf * Kg) (f * g)

theorem LipschitzWith.list_prod {α : Type u} {ι : Type x} [PseudoEMetricSpace α] (f : ι → Function.End α) (K : ι → NNReal) (h : ∀ (i : ι), LipschitzWith (K i) (f i)) (l : List ι) :

LipschitzWith (List.prod (List.map K l)) (List.prod (List.map f l))

The product of a list of Lipschitz continuous endomorphisms is a Lipschitz continuous endomorphism.

theorem LipschitzWith.pow_end {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} {K : NNReal} (h : LipschitzWith K f) (n : ℕ) :

LipschitzWith (K ^ n) (f ^ n)

theorem LipschitzOnWith.uniformContinuousOn {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) :

UniformContinuousOn f s

theorem LipschitzOnWith.continuousOn {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) :

ContinuousOn f s

theorem LipschitzOnWith.edist_le_mul_of_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (h : LipschitzOnWith K f s) {x : α} {y : α} (hx : x ∈ s) (hy : y ∈ s) {r : ENNReal} (hr : edist x y ≤ r) :

edist (f x) (f y) ≤ ↑K * r

theorem LipschitzOnWith.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) {x : α} {y : α} (hx : x ∈ s) (hy : y ∈ s) {d : ENNReal} (hd : edist x y < d / ↑K) :

edist (f x) (f y) < d

theorem LipschitzOnWith.comp {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {K : NNReal} {s : Set α} {f : α → β} {g : β → γ} {t : Set β} {Kg : NNReal} (hg : LipschitzOnWith Kg g t) (hf : LipschitzOnWith K f s) (hmaps : Set.MapsTo f s t) :

LipschitzOnWith (Kg * K) (g ∘ f) s

theorem LipschitzOnWith.prod {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {s : Set α} {f : α → β} {g : α → γ} {Kf : NNReal} {Kg : NNReal} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :

LipschitzOnWith (max Kf Kg) (fun (x : α) => (f x, g x)) s

If f and g are Lipschitz on s, so is the induced map f × g to the product type.

theorem LipschitzOnWith.ediam_image2_le {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α → β → γ) {K₁ : NNReal} {K₂ : NNReal} (s : Set α) (t : Set β) (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun (x : α) => f x b) s) (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) :

EMetric.diam (Set.image2 f s t) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t

theorem LipschitzWith.locallyLipschitz {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {K : NNReal} (hf : LipschitzWith K f) :

LocallyLipschitz f

A Lipschitz function is locally Lipschitz.

theorem LocallyLipschitz.id {α : Type u} [PseudoEMetricSpace α] :

LocallyLipschitz id

The identity function is locally Lipschitz.

theorem LocallyLipschitz.const {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) :

LocallyLipschitz fun (x : α) => b

Constant functions are locally Lipschitz.

theorem LocallyLipschitz.continuous {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (hf : LocallyLipschitz f) :

A locally Lipschitz function is continuous. (The converse is false: for example, $x ↦ \sqrt{x}$ is continuous, but not locally Lipschitz at 0.)

theorem LocallyLipschitz.comp {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : β → γ} {g : α → β} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :

LocallyLipschitz (f ∘ g)

The composition of locally Lipschitz functions is locally Lipschitz. -

theorem LocallyLipschitz.prod {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : α → β} (hf : LocallyLipschitz f) {g : α → γ} (hg : LocallyLipschitz g) :

LocallyLipschitz fun (x : α) => (f x, g x)

If f and g are locally Lipschitz, so is the induced map f × g to the product type.

theorem LocallyLipschitz.prod_mk_left {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (a : α) :

LocallyLipschitz (Prod.mk a)

theorem LocallyLipschitz.prod_mk_right {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) :

LocallyLipschitz fun (a : α) => (a, b)

theorem LocallyLipschitz.iterate {α : Type u} [PseudoEMetricSpace α] {f : α → α} (hf : LocallyLipschitz f) (n : ℕ) :

LocallyLipschitz f^[n]

theorem LocallyLipschitz.mul_end {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} {g : Function.End α} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :

LocallyLipschitz (f * g)

theorem LocallyLipschitz.pow_end {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} (h : LocallyLipschitz f) (n : ℕ) :

LocallyLipschitz (f ^ n)

theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {s' : Set α} {t : Set β} (hs' : s' ⊆ s) (hss' : s ⊆ closure s') (K : NNReal) (ha : ∀ a ∈ s', ContinuousOn (fun (y : β) => f (a, y)) t) (hb : ∀ b ∈ t, LipschitzOnWith K (fun (x : α) => f (x, b)) s) :

ContinuousOn f (s ×ˢ t)

Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical fiber” {a} × t, a ∈ s, and is Lipschitz continuous on each “horizontal fiber” s × {b}, b ∈ t with the same Lipschitz constant K. Then it is continuous on s × t. Moreover, it suffices to require continuity on vertical fibers for a from a subset s' ⊆ s that is dense in s.

The actual statement uses (Lipschitz) continuity of fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.

theorem continuousOn_prod_of_continuousOn_lipschitzOnWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : NNReal) (ha : ∀ a ∈ s, ContinuousOn (fun (y : β) => f (a, y)) t) (hb : ∀ b ∈ t, LipschitzOnWith K (fun (x : α) => f (x, b)) s) :

ContinuousOn f (s ×ˢ t)

Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical fiber” {a} × t, a ∈ s, and is Lipschitz continuous on each “horizontal fiber” s × {b}, b ∈ t with the same Lipschitz constant K. Then it is continuous on s × t.

The actual statement uses (Lipschitz) continuity of fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.

theorem continuous_prod_of_dense_continuous_lipschitzWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) {s : Set α} (hs : Dense s) (ha : ∀ a ∈ s, Continuous fun (y : β) => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun (x : α) => f (x, b)) :

Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical section” {a} × univ for a : α from a dense set. Suppose that it is Lipschitz continuous on each “horizontal section” univ × {b}, b : β with the same Lipschitz constant K. Then it is continuous.

The actual statement uses (Lipschitz) continuity of fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.

theorem continuous_prod_of_continuous_lipschitzWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) (ha : ∀ (a : α), Continuous fun (y : β) => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun (x : α) => f (x, b)) :

Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical section” {a} × univ, a : α, and is Lipschitz continuous on each “horizontal section” univ × {b}, b : β with the same Lipschitz constant K. Then it is continuous.

The actual statement uses (Lipschitz) continuity of fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.