English
If a function on α×β is continuous on a dense set of vertical fibers and Lipschitz on horizontal fibers uniformly, then it is continuous.
Русский
Если функция на α×β непрерывна на плотном подмножество вертикальных волокон и липшицева по горизонтальным волокнам с одинаковой константой, то она непрерывна.
LaTeX
$$$\\forall f:\\ α×β→γ, \\forall K, \\text{Dense } t, (ha: \\forall a, LipschitzOnWith K (\\lambda y. f(a,y)) t) (hb: \\forall b∈t, ContinuousOn (\\lambda x. f(x,b)) s) \\Rightarrow ContinuousOn f (s×t)$$$
Lean4
/-- 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. -/
theorem continuous_prod_of_continuous_lipschitzWith [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ]
(f : α × β → γ) (K : ℝ≥0) (ha : ∀ a, Continuous fun y => f (a, y)) (hb : ∀ b, LipschitzWith K fun x => f (x, b)) :
Continuous f :=
continuous_prod_of_dense_continuous_lipschitzWith f K dense_univ (fun _ _ ↦ ha _) hb
