map_nat_add' — Mathlib

English

For f ∈ F and n ∈ ℕ, f(n + x) = f(x) + n•b, i.e., nat-shift by a translates by n•b.

Русский

Для f ∈ F и n ∈ ℕ, f(n + x) = f(x) + n•b.

LaTeX

$$$\\forall f \\in F,\\forall n \\in \\mathbb{N},\\forall x \\in G:\\ f(n + x) = f(x) + n\\cdot b$$$

Lean4

@[scoped simp]
theorem map_nat_add' [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) (x : G) :
    f (↑n + x) = f x + n • b := by simpa using map_nsmul_add f n x

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