English
If f on α×β is continuous on vertical fibers for each a∈s and Lipschitz on horizontal fibers for each b∈t with constant K, then f is continuous on s×t.
Русский
Если на α×β функция непрерывна вдоль вертикальных волокон для каждого a∈s и липшицева по горизонтальным волокнам для каждого b∈t с константой K, то она непрерывна на s×t.
LaTeX
$$$\\forall f:\\ α×β→γ,\\forall s,t, (ha: \\forall a∈s, ContinuousOn (\\lambda y. f(a,y)) t) (hb: \\forall b∈t, LipschitzOnWith K (\\lambda x. f(x,b)) s) \\Rightarrow ContinuousOn f (s ×ˢ t)$$$
Lean4
/-- 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 continuousOn_prod_of_continuousOn_lipschitzOnWith [PseudoEMetricSpace α] [TopologicalSpace β]
[PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : ℝ≥0)
(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) :=
continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith f Subset.rfl subset_closure K ha hb
