map_ofNat_add' — Mathlib

English

For f ∈ F and n ∈ ℕ with n ≥ 2, f(ofNat(n) + x) = f(x) + ofNat(n)•b.

Русский

Для f ∈ F и n ∈ ℕ с n ≥ 2: f(ofNat(n) + x) = f(x) + ofNat(n)•b.

LaTeX

$$$\\forall f \\in F,\\forall n \\in \\mathbb{N},\\ [n \\ge 2] \\Rightarrow f(\\operatorname{ofNat}(n) + x) = f(x) + \\operatorname{ofNat}(n)\\,b$$$

Lean4

theorem map_ofNat_add' [AddCommMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ)
    [n.AtLeastTwo] (x : G) : f (ofNat(n) + x) = f x + ofNat(n) • b :=
  map_nat_add' f n x

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