map_comp_map — Mathlib

English

Given α-indexed families f,g,h with HasProduct, and q: f → g, q′: g → h, then Pi.map q ≫ Pi.map q′ = Pi.map (λ a, q(a) ≫ q′(a)).

Русский

Для семей f,g,h по индексу α с HasProduct, если q: f → g и q′: g → h, то Pi.map q идёт в Pi.map q′ как Pi.map (a ↦ q(a) ≫ q′(a)).

LaTeX

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

Lean4

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

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