dNext_comp_right — Mathlib

English

The right-hand compatibility of dNext with composition: dNext i (f ∘ g) = dNext i f ∘ g.f i.

Русский

Совместимость справа по отношению к композиции: dNext i (f ∘ g) = dNext i f ∘ g.f i.

LaTeX

$$dNext i (fun i j => f i j ≫ g.f j) = dNext i f ≫ g.f i$$

Lean4

theorem dNext_comp_right (f : ∀ i j, C.X i ⟶ D.X j) (g : D ⟶ E) (i : ι) :
    (dNext i fun i j => f i j ≫ g.f j) = dNext i f ≫ g.f i :=
  (assoc _ _ _).symm

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