inlX_d — Mathlib

English

For all i, j, k with hij, hjk, the composite inlX φ j i hij ≫ d φ i j equals −F.d j k ≫ inlX φ k j hjk plus φ.f j ≫ inrX φ j.

Русский

Для всех i, j, k с hij, hjk выполняется inlX φ j i hij ∘ d φ i j = −F.d j k ∘ inlX φ k j hjk + φ.f j ∘ inrX φ j.

LaTeX

$$$ inlX\\,\\phi\\,j\\,i\\,hij \\;\\circ\\; d\\,φ\\,i\\,j = -F.d\\,j\\,k \\;\\circ\\; inlX\\,φ\\,k\\,j\\,hjk + φ.f\\,j \\circ inrX\\,φ\\,j. $$$

Lean4

@[reassoc]
theorem inlX_d (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) :
    inlX φ j i hij ≫ d φ i j = -F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j :=
  by
  apply ext_to_X φ j k hjk
  · simp [d_fstX φ _ _ _ hij hjk]
  · simp [d_sndX φ _ _ hij]

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