map_lt_add_floor_translationNumber_add_one

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

← MathLib Explorer

English

For any f and x, f(x) < x + ⌊τ(f)⌋ + 1.

Русский

Для любых f и x выполнено f(x) < x + ⌊τ(f)⌋ + 1.

LaTeX

$$$$ \\forall f, \\forall x \\in \\mathbb{R}, \\ f(x) < x + \\Big\\lfloor \\tau f \\Big\\rfloor + 1. $$$$

Lean4

theorem map_lt_add_floor_translationNumber_add_one (x : ℝ) : f x < x + ⌊τ f⌋ + 1 :=
  by
  rw [add_assoc]
  norm_cast
  refine map_lt_of_translationNumber_lt_int _ ?_ _
  push_cast
  exact lt_floor_add_one _

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

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

Разделы

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

Аффилиация

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