map_sub_nat' — Mathlib

English

For f ∈ F and n ∈ ℕ, f(x - n) = f(x) - n·b, i.e., substracting n translates by n·b in the codomain.

Русский

Для f ∈ F и n ∈ ℕ: f(x - n) = f(x) - n·b.

LaTeX

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

Lean4

@[scoped simp]
theorem map_sub_nat' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ) :
    f (x - n) = f x - n • b := by simpa using map_sub_nsmul f x n

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