map_one_add

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_one_add (x : ℝ) : f (1 + x) = 1 + f x := by rw [add_comm, map_add_one, add_comm 1]

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

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

Разделы

Аффилиация

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