π_comp_eqToHom — Mathlib

English

Let f: J → C be a product. For j, j' ∈ J with w: j = j', the projection π_f(j) composed with the isomorphism eqToHom from the identification of j and j' equals π_f(j').

Русский

Пусть f: J → C имеет произведение. Пусть j, j' ∈ J и w: j = j'. Проекция π_f(j), композиция с изоморфизмом eqToHom от идентификации j и j' равны π_f(j').

LaTeX

$$$\forall {J} {f: J \to C} [HasProduct f] {j j' : J} (w: j = j'),\ Pi.\pi f j ≫ eqToHom (by simp [w]) = Pi.\pi f j'.$$

Lean4

@[reassoc]
theorem π_comp_eqToHom {J : Type*} (f : J → C) [HasProduct f] {j j' : J} (w : j = j') :
    Pi.π f j ≫ eqToHom (by simp [w]) = Pi.π f j' := by simp [*]

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