map_comp_map' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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