mapToComposableArrows_comp — Mathlib

English

The map to composable arrows respects composition: mapToComposableArrows(φ ∘ ψ) = mapToComposableArrows(φ) ∘ mapToComposableArrows(ψ).

Русский

Отображение в композиционные стрелки сохраняет композицию: mapToComposableArrows(φ ∘ ψ) = mapToComposableArrows(φ) ∘ mapToComposableArrows(ψ).

LaTeX

$$$\operatorname{mapToComposableArrows}(\varphi \circ \psi) = \operatorname{mapToComposableArrows}(\varphi) \circ \operatorname{mapToComposableArrows}(\psi)$$$

Lean4

@[simp]
theorem mapToComposableArrows_comp {S₁ S₂ S₃ : ShortComplex C} (φ : S₁ ⟶ S₂) (ψ : S₂ ⟶ S₃) :
    ShortComplex.mapToComposableArrows (φ ≫ ψ) =
      ShortComplex.mapToComposableArrows φ ≫ ShortComplex.mapToComposableArrows ψ :=
  by cat_disch

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