prodMap_coprod — Mathlib

English

A standard functorial property: composition under Prod.map preserves coprod structure in the sense that Tendsto holds between coprod and coprod.

Русский

Стандартное функторное свойство: композиция под Prod.map сохраняет копродуктивную структуру в смысле выполнения Tendsto между копродуктами.

LaTeX

$$$ \text{prodMap_coprod} \;: \text{Tendsto} (Prod.map f g) (a.coprod b) (c.coprod d) $$$

Lean4

theorem prodMap_coprod {δ : Type*} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β} {c : Filter γ} {d : Filter δ}
    (hf : Tendsto f a c) (hg : Tendsto g b d) : Tendsto (Prod.map f g) (a.coprod b) (c.coprod d) :=
  map_prodMap_coprod_le.trans (coprod_mono hf hg)

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