Theorems · Theorem · general topology

continuousOn_prod_of_continuousOn_lipschitzOnWith

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : NNReal),
  (∀ a ∈ s, ContinuousOn (fun y => f (a, y)) t) →
    (∀ 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.

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

6 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceTopologicalSpacePseudoEMetricSpace