comp_neg — Mathlib

English

Negation passes through composition in the second argument: z1 ∘ (-z2) = -(z1 ∘ z2).

Русский

Отрицание проходит через композицию во втором аргументе: z1 ∘ (-z2) = -(z1 ∘ z2).

LaTeX

$$$\\forall z_1, z_2, h,\\ z_1 \\circ (-z_2) \\\\; h = -(z_1 \\circ z_2 \\\\; h).$$$

Lean4

@[simp]
protected theorem comp_neg {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
    z₁.comp (-z₂) h = -z₁.comp z₂ h := by
  ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by cutsat), neg_v, comp_neg]

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