inlX_d' — Mathlib

English

If i, j are indices with hij, the relation inlX φ j i hij ≫ d φ i j = φ.f j ≫ inrX φ j holds.

Русский

Если i, j — индексы с hij, то inlX φ j i hij ∘ d φ i j = φ.f j ∘ inrX φ j.

LaTeX

$$$ inlX\\,\\phi\\,j\\,i\\,hij \\;\\circ\\; d\\,φ\\,i\\,j = φ.f\\,j \\circ inrX\\,φ\\,j. $$$

Lean4

@[reassoc]
theorem inlX_d' (i j : ι) (hij : c.Rel i j) (hj : ¬c.Rel j (c.next j)) : inlX φ j i hij ≫ d φ i j = φ.f j ≫ inrX φ j :=
  by
  apply ext_to_X' _ _ hj
  simp [d_sndX φ i j hij]

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