floor_sub_le_translationNumber

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

← MathLib Explorer

English

For any f and x, we have ⌊f(x) − x⌋ ≤ τ(f).

Русский

Для любого f и x верно ⌊f(x) − x⌋ ≤ τ(f).

LaTeX

$$$$ \\forall f, \\forall x \\in \\mathbb{R}, \\ \\Big\\lfloor f(x) - x \\Big\\rfloor \\le \\tau f. $$$$

Lean4

theorem floor_sub_le_translationNumber (x : ℝ) : ↑⌊f x - x⌋ ≤ τ f :=
  le_translationNumber_of_add_int_le f <| le_sub_iff_add_le'.1 (floor_le <| f x - x)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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