English
If f on α×β is such that it is continuous in the first coordinate for each second coordinate and Lipschitz in the second for the first, then f is continuous.
Русский
Если f на α×β непрерывна по первой координате для каждого второго и липшицева по второй координате в зависимости от первой, то f непрерывна.
LaTeX
$$$\\forall f:\\ Prod α β→γ$, $K$, $(ha: ∀ a, ContinuousOn (\\lambda y. f(a,y)) t)$ $(hb: ∀ b∈ t, LipschitzOnWith K (\\lambda x. f (x,b)) s) \\\\Rightarrow ContinuousOn f (s ×ˢ t)$$
Lean4
theorem continuous_prod_of_continuous_lipschitzWith' [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ]
(f : α × β → γ) (K : ℝ≥0) (ha : ∀ a, LipschitzWith K fun y => f (a, y)) (hb : ∀ b, Continuous fun x => f (x, b)) :
Continuous f :=
have : Continuous (f ∘ Prod.swap) := continuous_prod_of_continuous_lipschitzWith _ K hb ha
this.comp continuous_swap
