Theorems · Theorem · general topology

continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith

∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β},
  s' ⊆ s →
    s ⊆ closure s' →
      ∀ (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. 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.

Defined in

Mathlib.Topology.EMetricSpace.Lipschitz

Cited by

3 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpaceTopologicalSpacePseudoEMetricSpace