mapZ_comp — Mathlib

English

For arrows φ and ψ, mapZ respects composition: data.mapZ(φ ≫ ψ) = data.mapZ(φ) ≫ data.mapZ(ψ).

Русский

MapZ сохраняет композицию: mapZ(φ ≫ ψ) = mapZ(φ) ≫ mapZ(ψ).

LaTeX

$$$\forall φ, ψ, data.mapZ(φ \≫ ψ) = data.mapZ φ \≫ data.mapZ ψ$$$

Lean4

@[reassoc, simp]
theorem mapZ_comp {X'' Y'' : C} {h : X'' ⟶ Y''} (ψ : Arrow.mk g ⟶ Arrow.mk h) :
    data.mapZ (φ ≫ ψ) = data.mapZ φ ≫ data.mapZ ψ :=
  data.Z.map_comp _ _

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