English
The differential d on the connecting data is defined by L.d when both indices are nonnegative, by K.d when both indices are negative, and by special edge cases when indices straddle zero.
Русский
Дифференциал d на соединяющих данных задаётся как L.d при обеих индексациях неотрицательных, как K.d для обеих отрицательных и особые случаи на границе нуля.
LaTeX
$$$d: \forall n,m:\mathbb{Z}, X K L\; n \to X K L\; m,\; \text{defined piecewise by }\begin{cases} L.d\, n\, m, & n,m\ge 0, \\ K.d\, n\, m, & n,m<0, \\ \text{edge cases as in h}.\end{cases}$$$
Lean4
/-- Auxiliary definition for `ConnectData.cochainComplex`. -/
def d : ∀ (n m : ℤ), X K L n ⟶ X K L m
| .ofNat n, .ofNat m => L.d n m
| .negSucc n, .negSucc m => K.d n m
| .negSucc 0, .ofNat 0 => h.d₀
| .ofNat _, .negSucc _ => 0
| .negSucc _, .ofNat _ => 0
