map_add_one

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

For all real x, f(x+1) = f(x) + 1.

Русский

Для всякого x ∈ ℝ выполняется f(x+1) = f(x) + 1.

LaTeX

$$$\\forall x \\in \\mathbb{R},\\ f(x+1) = f(x) + 1$$$

Lean4

@[simp]
theorem map_add_one : ∀ x, f (x + 1) = f x + 1 :=
  f.map_add_one'

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

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

Разделы

Аффилиация

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