map'_comp_map — Mathlib

English

For f: α→C, g,h: β→C, p: β→α, q: ∀b, f(p b)→ g b, q': ∀b, g b→ h b, we have Pi.map' p q ≫ Pi.map q' = Pi.map' p (b ↦ q b ≫ q' b).

Русский

Для отображений f: α→C, g,h: β→C, p: β→α, q и q' как в формуле, существует тождество: Pi.map' p q ≫ Pi.map q' = Pi.map' p (b ↦ q b ≫ q' b).

LaTeX

$$$ \\Pi.map' p\\; q \\;≫\\; \\Pi.map q' = \\Pi.map' p (\\lambda b, q b \\;\\circ\\; q' b) $$$

Lean4

theorem map'_comp_map {f : α → C} {g h : β → C} [HasProduct f] [HasProduct g] [HasProduct h] (p : β → α)
    (q : ∀ (b : β), f (p b) ⟶ g b) (q' : ∀ (b : β), g b ⟶ h b) :
    Pi.map' p q ≫ Pi.map q' = Pi.map' p (fun b => q b ≫ q' b) := by ext; simp

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