d₂_eq — Mathlib

English

A standard expression for d2 in terms of ε2 and inclusion ιTotalOrZero.

Русский

Стандартное выражение для d2 через ε2 и включение ιTotalOrZero.

LaTeX

$$$K.d_2 c_{12} i_1 i_2 i_{12} = \\varepsilon_2 c_1 c_2 c_{12} \\langle i_1,i_2 \\rangle \\cdot ((K.X i_1).d i_2 i_2' \\circ ιTotalOrZero c_{12} i_1 i_2' i_{12} h')$$$

Lean4

theorem d₂_eq (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) (h' : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂'⟩ = i₁₂) :
    K.d₂ c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ • ((K.X i₁).d i₂ i₂' ≫ K.ιTotal c₁₂ i₁ i₂' i₁₂ h') :=
  totalAux.d₂_eq _ _ _ h _ _

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