map'_eq — Mathlib

English

If p = p' and q, q' are related by eqToHom along the equality, then Pi.map' p q = Pi.map' p' q'.

Русский

Если p = p' и q, q' связаны равенством через eqToHom, то Pi.map' p q = Pi.map' p' q'.

LaTeX

$$$\text{If } p = p' \text{ and } ∀ b, eqToHom (hp\,\!\, b) ≫ q b = q' b,\ Pi.map' p q = Pi.map' p' q'.$$$

Lean4

theorem map'_eq {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] {p p' : β → α} {q : ∀ (b : β), f (p b) ⟶ g b}
    {q' : ∀ (b : β), f (p' b) ⟶ g b} (hp : p = p') (hq : ∀ (b : β), eqToHom (hp ▸ rfl) ≫ q b = q' b) :
    Pi.map' p q = Pi.map' p' q' := by cat_disch

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