English
A swapped version: if f on α×β satisfies fiber conditions after swapping coordinates, it is continuous on the swapped product.
Русский
Переписанная версия после перестановки координат: если f удовлетворяет условиям по волокнам после перестановки координат, то она непрерывна на перестановке произведения.
LaTeX
$$$\\forall f:\\ Prod α β→γ, {s} {t} (ht': t'⊆t) (htt': t ⊆ closure t') (K) (ha: ∀ a∈s, LipschitzOnWith K (\\lambda y. f(a,y)) t) (hb: ∀ b∈t', ContinuousOn (\\lambda x. f (x,b)) s) \\\\Rightarrow ContinuousOn f (s ×ˢ t)$$
Lean4
theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith' [TopologicalSpace α] [PseudoEMetricSpace β]
[PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t t' : Set β} (ht' : t' ⊆ t) (htt' : t ⊆ closure t') (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_subset_closure_continuousOn_lipschitzOnWith _ ht' htt' K hb ha
this.comp continuous_swap.continuousOn (mapsTo_swap_prod _ _)
