shiftₗ_apply

Mathlib.Algebra.Group.ForwardDiff

URI: https://scilib.ai/kg/mathlib#fwdDiff_aux.shiftₗ_apply

English

For any f: M → G and y ∈ M, the shifted function satisfies (shift_h f)(y) = f(y + h).

Русский

Для любой функции f: M → G и элемента y ∈ M выполняется (shift_h f)(y) = f(y + h).

LaTeX

$$$ (\text{shift}_h f)(y) = f(y + h) $$$

Lean4

theorem shiftₗ_apply (f : M → G) (y : M) : shiftₗ M G h f y = f (y + h) := by simp [shiftₗ, fwdDiff]

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

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

Разделы

Аффилиация

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