prodMap — Mathlib

English

Let f: X → Y and g: U → V be continuous maps. Then the map (x,y) ↦ (f(x), g(y)) from X × U to Y × V is continuous.

Русский

Пусть f: X → Y и g: U → V — непрерывные отображения. Тогда отображение (x, y) ↦ (f(x), g(y)) из X × U в Y × V непрерывно.

LaTeX

$$$f: X \to Y,\ g: U \to V \Rightarrow \operatorname{Continuous}(\mathrm{ProdMap}(f,g))$$$

Lean4

/-- Given two continuous maps `f` and `g`, this is the continuous map `(x, y) ↦ (f x, g y)`. -/
@[simps]
def prodMap (f : C(α₁, α₂)) (g : C(β₁, β₂)) : C(α₁ × β₁, α₂ × β₂) where toFun := Prod.map f g

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