app_apply — Mathlib

English

For any X, the derivation component of app(d) at X applied to b is the same as d's component at X applied to b: (d.app X).d b = d.d b.

Русский

Для любого X компонент деривации app(d) в X на элемент b совпадает с компонентой d в X: (d.app X).d b = d.d b.

LaTeX

$$$(d.app X).d\, b = d.d\, b$$$

Lean4

@[simp]
theorem app_apply (d : M.Derivation' φ') {X : Dᵒᵖ} (b : R.obj X) : (d.app X).d b = d.d b :=
  rfl

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