comp_sub — Mathlib

English

The composition distributes over subtraction in the second argument: z1 ∘ (z2 - z2') = z1 ∘ z2 - z1 ∘ z2'.

Русский

Композиция по второй координате дистрибутивна по вычитанию: z1 ∘ (z2 - z2') = z1 ∘ z2 - z1 ∘ z2'.

LaTeX

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

Lean4

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

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