fwdDiff_iter_add — Mathlib

English

The nth iterate of the forward difference is additive: Δ_h^[n] (f + g) = Δ_h^[n] f + Δ_h^[n] g.

Русский

n-я итерация прямой разности распределяется по сложению: Δ_h^[n] (f + g) = Δ_h^[n] f + Δ_h^[n] g.

LaTeX

$$$ \Delta_h^{[n]} (f + g) = \Delta_h^{[n]} f + \Delta_h^{[n]} g $$$

Lean4

@[simp]
theorem fwdDiff_iter_add (f g : M → G) (n : ℕ) : Δ_[h]^[n] (f + g) = Δ_[h]^[n] f + Δ_[h]^[n] g := by
  simpa only [coe_fwdDiffₗ_pow] using map_add (fwdDiffₗ M G h ^ n) f g

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