truncLE'Map_comp — Mathlib

English

The truncLE'Map respects composition: truncLE'Map(φ ∘ φ') e = truncLE'Map φ e ∘ truncLE'Map φ' e.

Русский

TruncLE'Map сохраняет композицию: truncLE'Map(φ ∘ φ') e = truncLE'Map φ e ∘ truncLE'Map φ' e.

LaTeX

$$$\mathrm{truncLE'Map}(\phi \circ \phi', e) = \mathrm{truncLE'Map}(\phi, e) \circ \mathrm{truncLE'Map}(\phi', e)$$$

Lean4

@[reassoc, simp]
theorem truncLE'Map_comp : truncLE'Map (φ ≫ φ') e = truncLE'Map φ e ≫ truncLE'Map φ' e :=
  (unopFunctor C c.symm).congr_map
    (congr_arg Quiver.Hom.op (truncGE'Map_comp ((opFunctor C c').map φ'.op) ((opFunctor C c').map φ.op) e.op))

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