dFrom_comp_xNextIsoSelf — Mathlib

English

If not c.Rel i (c.next i), then dFrom i ≫ (xNextIsoSelf h).hom = 0 for the appropriate h.

Русский

Если не выполняется c.Rel i (c.next i), тогда dFrom i \\\\circ (xNextIsoSelf h).hom = 0.

LaTeX

$$$\\\\neg c.Rel \\\\ i \\\\ (c.next i) \\\\Rightarrow C.dFrom i \\\\circ (C.xNextIsoSelf h).hom = 0$$$

Lean4

@[reassoc]
theorem dFrom_comp_xNextIsoSelf {i : ι} (h : ¬c.Rel i (c.next i)) : C.dFrom i ≫ (C.xNextIsoSelf h).hom = 0 := by
  simp [h]
    -- This is not a simp lemma; the LHS already simplifies.

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