map'_comp_π — Mathlib

English

For f: α → C and g: β → C with product structures, and p, q, b as in the statement, Pi.map' p q ≫ Pi.π g b = Pi.π f (p b) ≫ q b.

Русский

Для f: α → C и g: β → C с произведениями, выполняется Pi.map' p q ≫ Pi.π g b = Pi.π f (p b) ≫ q b.

LaTeX

$$$\Pi.map' p q \;\;\gg\;\Pi.\pi g b = \Pi.\pi f (p b) \;\gg\; q b$$$

Lean4

@[reassoc (attr := simp)]
theorem map'_comp_π {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] (p : β → α) (q : ∀ (b : β), f (p b) ⟶ g b)
    (b : β) : Pi.map' p q ≫ Pi.π g b = Pi.π f (p b) ≫ q b :=
  limit.lift_π _ _

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