assoc — Mathlib

English

The projection π is associative with respect to the total complex, i.e., (π ∘ (π ∘ id)) = (π ∘ (id ∘ π)) up to the total complex structure.

Русский

Проекция π ассоциативна в отношении полного комплекса: (π ∘ (π ∘ id)) = (π ∘ (id ∘ π)) в рамках структуры полного комплекса.

LaTeX

$$$\\text{assoc}(π,c_1,c_2,c_{12},c_3, c_{23}, c)=π(c_1,c_2,c_{12})∘π(⋯)=π(⋯)$$$

Lean4

theorem assoc (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) :
    π c₁₂ c₃ c ⟨π c₁ c₂ c₁₂ ⟨i₁, i₂⟩, i₃⟩ = π c₁ c₂₃ c ⟨i₁, π c₂ c₃ c₂₃ ⟨i₂, i₃⟩⟩ := by apply Associative.assoc

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