prevD_comp_right — Mathlib

English

Compatibility of prevD with right composition: prevD j (f ∘ g) = prevD j f ∘ g.f j.

Русский

Совместимость prevD с правым разложением: prevD j (f ∘ g) = prevD j f ∘ g.f j.

LaTeX

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

Lean4

theorem prevD_comp_right (f : ∀ i j, C.X i ⟶ D.X j) (g : D ⟶ E) (j : ι) :
    (prevD j fun i j => f i j ≫ g.f j) = prevD j f ≫ g.f j :=
  by
  dsimp [prevD]
  simp only [assoc, g.comm]

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