commute_nat_add — Mathlib

English

For every natural n, f commutes with the map x ↦ x + n, i.e., f(x + n) = f(x) + n for all x in ℝ.

Русский

Для каждого натурального n функция f commuting со сдвигом на n, то есть f(x + n) = f(x) + n для всех x ∈ ℝ.

LaTeX

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

Lean4

theorem commute_nat_add (n : ℕ) : Function.Commute f (n + ·) := by
  simpa only [nsmul_one, add_left_iterate] using Function.Commute.iterate_right f.map_one_add n

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