continuous_prod_of_discrete_right

English

If β is discrete, continuous of f: α × β → γ is equivalent to continuous of x ↦ f(x,b) for each b.

Русский

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

LaTeX

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

Lean4

theorem continuous_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} :
    Continuous f ↔ ∀ b, Continuous (f ⟨·, b⟩) := by simp_rw [← continuousOn_univ];
  exact continuousOn_prod_of_discrete_right

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