English
Swapped version of a fiberwise result: if on α×β with swapped indices, conditions hold, then continuity on s×t.
Русский
Перестановка индексов в неравенстве; если условия выполняются на α×β после перестановки, тогда непрерывность на s×t.
LaTeX
$$$\\forall f:\\ Prod α β→γ, {s} {t} (K) (ha: ∀ a, a∈ s → LipschitzOnWith K (\\lambda y. f (a,y)) t) (hb: ∀ b∈ t, ContinuousOn (\\lambda x. f (x,b)) s) \\\\Rightarrow ContinuousOn f (Set.instSProd.sprod s t)$$
Lean4
theorem continuousOn_prod_of_continuousOn_lipschitzOnWith' [TopologicalSpace α] [PseudoEMetricSpace β]
[PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : ℝ≥0)
(ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t) (hb : ∀ b ∈ t, ContinuousOn (fun x => f (x, b)) s) :
ContinuousOn f (s ×ˢ t) :=
have : ContinuousOn (f ∘ Prod.swap) (t ×ˢ s) := continuousOn_prod_of_continuousOn_lipschitzOnWith _ K hb ha
this.comp continuous_swap.continuousOn (mapsTo_swap_prod _ _)
