dNext_comp_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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