prodMap — Mathlib

English

Let f: X → Y and g: Z → W be maps between topological spaces. If f and g are inducing, then the product map Prod.map f g: X × Z → Y × W is inducing.

Русский

Пусть f: X → Y и g: Z → W — отображения между топологическими пространствами. Если f и g индуцирующие, то произведение отображений Prod.map f g: X × Z → Y × W индуцирующее.

LaTeX

$$$\IsInducing(f) \land \IsInducing(g) \Rightarrow \IsInducing(\mathrm{Prod.map} f g)$$$

Lean4

theorem prodMap {f : X → Y} {g : Z → W} (hf : IsInducing f) (hg : IsInducing g) : IsInducing (Prod.map f g) :=
  isInducing_iff_nhds.2 fun (x, z) => by
    simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap, hg.nhds_eq_comap, prod_comap_comap_eq]

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