fwdDiff_add

Mathlib.Algebra.Group.ForwardDiff

URI: https://scilib.ai/kg/mathlib#fwdDiff_add

English

The forward-difference operator is additive: Δ_h(f + g) = Δ_h f + Δ_h g.

Русский

Оператор приращения по сдвигу h аддитивен: Δ_h(f + g) = Δ_h f + Δ_h g.

LaTeX

$$$\Delta_{h}(f + g) = \Delta_{h} f + \Delta_{h} g,$$$

Lean4

@[simp]
theorem fwdDiff_add (h : M) (f g : M → G) : Δ_[h] (f + g) = Δ_[h] f + Δ_[h] g :=
  add_sub_add_comm ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru