map_add_ofNat — Mathlib

English

Let f ∈ F, x ∈ G, n ∈ ℕ with n ≥ 2. Then f(x + ofNat(n)) = f(x) + ofNat(n).

Русский

Пусть f ∈ F, x ∈ G, n ∈ ℕ с n ≥ 2. Тогда f(x + ofNat(n)) = f(x) + ofNat(n).

LaTeX

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

Lean4

theorem map_add_ofNat [AddMonoidWithOne G] [AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (x : G) (n : ℕ)
    [n.AtLeastTwo] : f (x + ofNat(n)) = f x + ofNat(n) :=
  map_add_nat f x n

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