map_ofNat_add — Mathlib

English

For f ∈ F and a = 1, b = 1, f(ofNat(n) + x) = f(x) + ofNat(n).

Русский

Для f ∈ F и a = 1, b = 1: f(ofNat(n) + x) = f(x) + ofNat(n).

LaTeX

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

Lean4

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

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