shiftₗ_pow_apply — Mathlib

English

For any f: M → G, k ∈ ℕ, and y ∈ M, we have ((shift_h)^k f)(y) = f(y + k·h).

Русский

Для любой функции f: M → G, k ∈ ℕ и y ∈ M выполнено ((shift_h)^k f)(y) = f(y + k·h).

LaTeX

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

Lean4

theorem shiftₗ_pow_apply (f : M → G) (k : ℕ) (y : M) : (shiftₗ M G h ^ k) f y = f (y + k • h) := by
  induction k generalizing f with
  | zero => simp
  | succ k IH => simp [pow_add, IH (shiftₗ M G h f), shiftₗ_apply, add_assoc, add_nsmul]

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