α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
ha : ∀ (a : α), ContinuousOn (fun y => f (a, y)) univ
hb : ∀ (b : β), LipschitzOnWith K (fun x => f (x, b)) univ
⊢ ContinuousOn f (univ ×ˢ univ)
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
ha : ∀ (a : α), Continuous fun y => f (a, y)
hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)
⊢ Continuous f
simp only [continuous_iff_continuousOn_univ, ← univ_prod_univ, ← lipschitz_on_univ] at *
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
ha : ∀ (a : α), ContinuousOn (fun y => f (a, y)) univ
hb : ∀ (b : β), LipschitzOnWith K (fun x => f (x, b)) univ
⊢ ContinuousOn f (univ ×ˢ univ)
exact continuousOn_prod_of_continuousOn_lipschitz_on f K (fun a _ => ha a) fun b _ => hb b