shape_f — Mathlib

English

For a bicomplex K, if i1 is not related to i1' in c1 (i.e., Not c1.Rel i1 i1'), then the horizontal differential component (K.d i1 i1').f i2 is zero for all i2.

Русский

Для биокомплексa K если i1 не связан с i1' в c1, то горизонтальный компонент дифференциала равен нулю для всех i2.

LaTeX

$$$\text{shape}_1(i_1,i_1',\, \neg c_1.Rel(i_1,i_1')) \Rightarrow (K.d i_1 i_1').f i_2 = 0$$$

Lean4

theorem shape_f (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' : I₁) (h : ¬c₁.Rel i₁ i₁') (i₂ : I₂) :
    (K.d i₁ i₁').f i₂ = 0 := by rw [K.shape _ _ h, zero_f]

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