prodMk — Mathlib

English

If f: Z → X and g: Z → Y are continuous, then the map z ↦ (f(z), g(z)) is continuous.

Русский

Если f: Z → X и g: Z → Y непрерывны, то z ↦ (f(z), g(z)) непрерывно на Z.

LaTeX

$$$\text{Continuous}(f) \land \text{Continuous}(g) \Rightarrow \text{Continuous}(\lambda z, (f(z), g(z)))$$$

Lean4

@[continuity, fun_prop]
theorem prodMk {f : Z → X} {g : Z → Y} (hf : Continuous f) (hg : Continuous g) : Continuous fun x => (f x, g x) :=
  continuous_prodMk.2 ⟨hf, hg⟩

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