lt_map_of_int_lt_translationNumber

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

← MathLib Explorer

English

If n ≤ τ(f) (in integers), then x + n ≤ f(x) for all x.

Русский

Если n ≤ τ(f) (целое число), то ∀x, x + n ≤ f(x).

LaTeX

$$$$ \\forall f, \\forall n \\in \\mathbb{Z}, \\ n \\le \\tau f \\Rightarrow \\forall x \\in \\mathbb{R}, \\ x + n \\le f(x). $$$$

Lean4

theorem lt_map_of_int_lt_translationNumber {n : ℤ} (h : ↑n < τ f) (x : ℝ) : x + n < f x :=
  not_le.1 <| mt f.translationNumber_le_of_le_add_int <| not_le.2 h

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

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

Разделы

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

Аффилиация

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