fwdDiff_comp_add

Mathlib.Algebra.Group.ForwardDiff

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

English

For f: M → G and m ∈ M, Δ_h (f(r + m)) y = (Δ_h f)(y + m).

Русский

Для f: M → G и m ∈ M, Δ_h (f(r + m)) = (Δ_h f)(y + m).

LaTeX

$$$ \Delta_h (f (\cdot + m)) (y) = (\Delta_h f)(y + m) $$$

Lean4

theorem fwdDiff_comp_add (f : M → G) (m : M) (y : M) : Δ_[h] (fun r ↦ f (r + m)) y = (Δ_[h] f) (y + m) :=
  fwdDiff_iter_comp_add h f m 1 y

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

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

Разделы

Аффилиация

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