map_nat_add

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

For all x ∈ ℝ and n ∈ ℕ, f(n + x) = n + f(x).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_nat_add (n : ℕ) (x : ℝ) : f (n + x) = n + f x :=
  f.map_int_add n x

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

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

Разделы

Аффилиация

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