continuous_prod_of_discrete_left — Mathlib

English

If α is discrete, then a function f: α × β → γ is continuous iff for every a, the function x ↦ f(a,x) is continuous.

Русский

Если α дискретно, то функция f: α × β → γ непрерывна тогда и только тогда, когда для каждого a функция x ↦ f(a,x) непрерывна.

LaTeX

$$$$\text{Continuous } f \iff \forall a, \text{Continuous }\bigl(x \mapsto f(a,x)\bigr). $$$$

Lean4

/-- If a function `f a b` is such that `y ↦ f a b` is continuous for all `a`, and `a` lives in a
discrete space, then `f` is continuous, and vice versa. -/
theorem continuous_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} :
    Continuous f ↔ ∀ a, Continuous (f ⟨a, ·⟩) := by simp_rw [← continuousOn_univ];
  exact continuousOn_prod_of_discrete_left

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