d_comp_eqToHom — Mathlib

English

If f = g, then for all indices i, you have f.f i = g.f i.

Русский

Если f = g, тогда для всех индексов i выполняется f.f i = g.f i.

LaTeX

$$$\\\\forall {i} \\\\; (f = g) \\\\Rightarrow f.f i = g.f i$$$

Lean4

/-- If `C.d i j` and `C.d i j'` are both allowed, then we must have `j = j'`,
and so the differentials only differ by an `eqToHom`.
-/
@[simp]
theorem d_comp_eqToHom {i j j' : ι} (rij : c.Rel i j) (rij' : c.Rel i j') :
    C.d i j' ≫ eqToHom (congr_arg C.X (c.next_eq rij' rij)) = C.d i j :=
  by
  obtain rfl := c.next_eq rij rij'
  simp only [eqToHom_refl, comp_id]

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