map_int_add

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

For every integer m and every real x, f(m + x) = m + f(x).

Русский

Для каждого целого m и каждого x ∈ ℝ выполняется f(m + x) = m + f(x).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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