prevD_comp_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem prevD_comp_left (f : C ⟶ D) (g : ∀ i j, D.X i ⟶ E.X j) (j : ι) :
    (prevD j fun i j => f.f i ≫ g i j) = f.f j ≫ prevD j g :=
  assoc _ _
    _
      -- This is not a simp lemma; the LHS already simplifies.

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