map_add_int

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

URI: https://scilib.ai/kg/mathlib#CircleDeg1Lift.map_add_int

English

For all x ∈ ℝ and m ∈ ℤ, f(x + m) = f(x) + m.

Русский

Для всех x ∈ ℝ и m ∈ ℤ выполняется f(x + m) = f(x) + m.

LaTeX

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

Lean4

@[simp]
theorem map_add_int (x : ℝ) (m : ℤ) : f (x + m) = f x + m :=
  f.commute_add_int m x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru