continuous_prodMk — Mathlib

English

A map x ↦ (f x, g x) into Y × Z is continuous iff f and g are continuous individually.

Русский

отображение x ↦ (f x, g x) непрерывно тогда и только тогда, когда f и g каждый по отдельности непрерывны.

LaTeX

$$$\\text{Continuous}\\left( x \\mapsto (f x, g x)\\right) \\iff \\mathrm{Continuous}(f) \\wedge \\mathrm{Continuous}(g).$$$

Lean4

@[simp]
theorem continuous_prodMk {f : X → Y} {g : X → Z} : (Continuous fun x => (f x, g x)) ↔ Continuous f ∧ Continuous g :=
  continuous_inf_rng.trans <| continuous_induced_rng.and continuous_induced_rng

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