ι_D₁ — Mathlib

English

The inclusion maps satisfy the D₁ relation with the differential d₁.

Русский

Включающие отображения удовлетворяют отношение D₁ с дифференциалом d₁.

LaTeX

$$ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ D₁ K₁ K₂ F c j j' = d₁ K₁ K₂ F c i₁ i₂ j'$$

Lean4

@[reassoc (attr := simp)]
theorem ι_D₁ : ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ D₁ K₁ K₂ F c j j' = d₁ K₁ K₂ F c i₁ i₂ j' := by
  apply HomologicalComplex₂.ι_D₁

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