map'_eq — Mathlib

English

If p = p', and q a ≫ eqToHom (hp ▸ rfl) = q' a for all a, then Sigma.map' p q = Sigma.map' p' q'.

Русский

Если p = p′ и q a ≫ eqToHom(...) = q′ a для всех a, то Sigma.map' p q = Sigma.map' p' q'.

LaTeX

$$$p = p' \\Rightarrow \\forall a,\\ q a \\;\\!\\!\\!\\!\\!\\;= q' a \\text{ up to } eqToHom$ implies $\\Sigma\\text{map}' p q = \\Sigma\\text{map}' p' q'.$$$

Lean4

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

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