isInducing_prodMap — Mathlib

English

If f and g are inducing maps, then the product map prod.map f g is inducing with respect to the product topology.

Русский

Если f и g индуктивные отображения, тогда prod.map f g индуктивен относительно топологий произведения.

LaTeX

$$$\\text{IsInducing}(\\mathrm{Limits.prod.map} f g)$$$

Lean4

theorem isInducing_prodMap {W X Y Z : TopCat.{u}} {f : W ⟶ X} {g : Y ⟶ Z} (hf : IsInducing f) (hg : IsInducing g) :
    IsInducing (Limits.prod.map f g) := by
  constructor
  simp_rw [prod_topology, induced_inf, induced_compose, ← coe_comp, prod.map_fst, prod.map_snd, coe_comp, ←
    induced_compose (g := f), ← induced_compose (g := g)]
  rw [← hf.eq_induced, ← hg.eq_induced]

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