d_sndX — Mathlib

English

For all i, j, the differential d φ i j followed by sndX φ j equals fstX φ i j hij composed with φ.f j plus sndX φ i composed with G.d i j.

Русский

Для всех i, j дифференциал d φ i j затем sndX φ j равен fstX φ i j hij ∘ φ.f j плюс sndX φ i ∘ G.d i j.

LaTeX

$$$ d\\,φ\\,i\\,j \\;\\circ\\; sndX\\,φ\\,j = fstX\\,φ\\,i\\,j\\,hij \\circ φ.f\\,j + sndX\\,φ\\,i \\circ G.d\\,i\\,j. $$$

Lean4

@[reassoc]
theorem d_sndX (i j : ι) (hij : c.Rel i j) : d φ i j ≫ sndX φ j = fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j :=
  by
  dsimp [d]
  split_ifs with hij <;> simp

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