prodMap — Mathlib

English

If f and g are continuous, then the product map Prod.map f g is continuous.

Русский

Если f и g непрерывны, то отображение произведения Prod.map f g непрерывно.

LaTeX

$$$\text{Continuous}(f) \rightarrow \text{Continuous}(g) \rightarrow \text{Continuous}(\text{Prod.map } f g)$$$

Lean4

@[continuity, fun_prop]
theorem prodMap {f : Z → X} {g : W → Y} (hf : Continuous f) (hg : Continuous g) : Continuous (Prod.map f g) :=
  hf.fst'.prodMk hg.snd'

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