eqToHom_f' — Mathlib

English

For any morphism f: X → Y of differential objects, and indices i, the equality X.objEqToHom h ≫ f.f i = f.f i ≫ Y.objEqToHom h holds when h identifies i with i via index equality

Русский

Для морфизма f: X → Y между дифференциальными объектами верно равенство X.objEqToHom h ≫ f.f i = f.f i ≫ Y.objEqToHom h при совпадении индексов через h

LaTeX

$$$\forall f: X \to Y, \forall i,j,\; h: i=j \Rightarrow X.objEqToHom h \;\circ\; f.f j = f.f i \;\circ\; Y.objEqToHom h$$$

Lean4

@[reassoc]
theorem eqToHom_f' {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) :
    X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h := by cases h; simp

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