map_fract_sub_fract_eq

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

For all x ∈ ℝ, f(fract(x)) − fract(x) = f(x) − x.

Русский

Для всех x ∈ ℝ верно: f(fract(x)) − fract(x) = f(x) − x.

LaTeX

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

Lean4

@[simp]
theorem map_fract_sub_fract_eq (x : ℝ) : f (fract x) - fract x = f x - x := by
  rw [Int.fract, f.map_sub_int, sub_sub_sub_cancel_right]

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

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

Разделы

Аффилиация

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