fwdDiff_const — Mathlib

English

Let h ∈ M and g ∈ G. If F: M → G is the constant function F(x) = g, then the forward difference Δ_h F is identically zero: Δ_h F = 0 as a function M → G.

Русский

Пусть h ∈ M и g ∈ G. Если F: M → G — константная функция F(x) = g, то передняя разность Δ_h F тождественно равна нулю: Δ_h F = 0 как функция M → G.

LaTeX

$$$ \Delta_h (x \mapsto g) = 0 $$$

Lean4

@[simp]
theorem fwdDiff_const (g : G) : Δ_[h] (fun _ ↦ g : M → G) = fun _ ↦ 0 :=
  funext fun _ ↦ sub_self g

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