map_comp_map' — Mathlib

English

Two Sigma maps compose compatibly: Sigma.map q followed by Sigma.map' p q' equals Sigma.map' p (a ↦ q a ≫ q'(p a)).

Русский

Две композиции Sigma совместимы: Sigma.map q затем Sigma.map' p q' равны Sigma.map' p (a → q a ≫ q'(p a)).

LaTeX

$$$\\Sigma\\text{map} \\; q \\;\\gg\\; \\Sigma\\text{map}' p q' = \\Sigma\\text{map}' p (a \\mapsto q a \\gg q'(p a))$$$

Lean4

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

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