commute_sub_int — Mathlib

English

For every integer n, f(x − n) = f(x) − n for all x.

Русский

Для каждого целого n выполняется f(x − n) = f(x) − n для всех x.

LaTeX

$$$ \forall n \in \mathbb{Z}, \forall x \in \mathbb{R}, \; f(x - n) = f(x) - n. $$$

Lean4

theorem commute_sub_int (n : ℤ) : Function.Commute f (· - n) := by
  simpa only [sub_eq_add_neg] using
    (f.commute_add_int n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv

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