map_sub_nat

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_sub_nat (x : ℝ) (n : ℕ) : f (x - n) = f x - n :=
  f.map_sub_int x n

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

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

Разделы

Аффилиация

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