English
If f is continuous along vertical lines from a dense set and Lipschitz along horizontal lines with the same K, then f is continuous on the whole product.
Русский
Если вдоль вертикальных линий из плотного множества f непрерывна и вдоль горизонтальных линий липшицева с той же константой K, то f непрерывна на всей произведенной области.
LaTeX
$$$f:\\ α×β→γ,\ K≥0,\ hs: Dense s,\ ha: \\forall a∈s, Continuous (\\lambda y, f(a,y)), hb: \\forall b, LipschitzWith K (\\lambda x, f(x,b))$, Continuous f.$$
Lean4
/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical section”
`{a} × univ` for `a : α` from a dense set. Suppose that it is Lipschitz continuous on each
“horizontal section” `univ × {b}`, `b : β` with the same Lipschitz constant `K`. Then it is
continuous.
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 continuous_prod_of_dense_continuous_lipschitzWith [PseudoEMetricSpace α] [TopologicalSpace β]
[PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) {s : Set α} (hs : Dense s)
(ha : ∀ a ∈ s, Continuous fun y => f (a, y)) (hb : ∀ b, LipschitzWith K fun x => f (x, b)) : Continuous f :=
by
simp only [← continuousOn_univ, ← univ_prod_univ, ← lipschitzOnWith_univ] at *
exact
continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith f (subset_univ _) hs.closure_eq.ge K ha fun b _ =>
hb b
