continuous_prod_of_dense_continuous_lipschitzWith'

English

A variant: if f on α×β has a dense set of β such that Lipschitz in y for all a, and continuous in x for all b in t, then f is continuous.

Русский

Вариант: если f на α×β имеет плотный набор β так, что липшицевость по y для всех a, и непрерывность по x для всех b в t, тогда f непрерывна.

LaTeX

$$$\\forall f: α×β→γ$, $K$, $ht: Dense t$, $(ha: ∀ a, LipschitzWith K (\\lambda y. f(a,y))$ t) $(hb: ∀ b ∈ t, Continuous (\\lambda x. f (x,b))) \\Rightarrow Continuous f$$$

Lean4

theorem continuous_prod_of_dense_continuous_lipschitzWith' [TopologicalSpace α] [PseudoEMetricSpace β]
    [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) {t : Set β} (ht : Dense t)
    (ha : ∀ a, LipschitzWith K fun y => f (a, y)) (hb : ∀ b ∈ t, Continuous fun x => f (x, b)) : Continuous f :=
  have : Continuous (f ∘ Prod.swap) := continuous_prod_of_dense_continuous_lipschitzWith _ K ht hb ha
  this.comp continuous_swap

Похожие утверждения