map'_comp_map' — Mathlib

English

For f: α → C, g: β → C and h: γ → C with HasProduct, p: β → α, p': γ → β, q, q' as described, Pi.map' p q ≫ Pi.map' p' q' = Pi.map' (p ∘ p') (λ c, q(p' c) ≫ q' c).

Русский

Для f: α → C, g: β → C и h: γ → C с HasProduct, p: β → α, p': γ → β, выполняется Pi.map' p q ≫ Pi.map' p' q' = Pi.map' (p ∘ p') (λ c, q(p' c) ≫ q' c).

LaTeX

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

Lean4

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

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