coe_sub — Mathlib

English

For Lie Derivations D1 and D2, the underlying function of their difference coincides with the difference of the underlying functions: the function obtained from D1 − D2 equals the pointwise difference D1 − D2 as functions.

Русский

Для производных Ли D1 и D2 соответствующая функция разности совпадает с разностью соответствующих функций: функция D1 − D2 равна точечной разности D1 и D2.

LaTeX

$$$\uparrow(D_1 - D_2) = D_1 - D_2$$$

Lean4

@[simp]
theorem coe_sub (D1 D2 : LieDerivation R L M) : ⇑(D1 - D2) = D1 - D2 :=
  rfl

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