Theorems · Theorem · general topology

continuous_prod_of_continuous_lipschitzWith

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

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.

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceTopologicalSpacePseudoEMetricSpace