trans — Mathlib

English

As above, transitivity for OneCochain cohomology relations: γ1 γ2 α → γ2 γ3 β ⇒ γ1 γ3 (β * α).

Русский

Как выше, транзитивность отношений когомологичности OneCochain: γ1 γ2 α и γ2 γ3 β ⇒ γ1 γ3 (β * α).

LaTeX

$$OneCohomologyRelation γ1 γ3 (β * α)$$

Lean4

theorem trans {γ₁ γ₂ γ₃ : OneCochain G U} {α β : ZeroCochain G U} (h₁₂ : OneCohomologyRelation γ₁ γ₂ α)
    (h₂₃ : OneCohomologyRelation γ₂ γ₃ β) : OneCohomologyRelation γ₁ γ₃ (β * α) := fun i j T a b ↦
  by
  dsimp
  rw [map_mul, map_mul, mul_assoc, h₁₂ i j a b, ← mul_assoc, h₂₃ i j a b, mul_assoc]

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