lt_map_of_nat_lt_translationNumber

Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

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

English

For natural n, if n < τ(f), then x + n < f(x).

Русский

Для натурального n, если n < τ(f), тогда x + n < f(x).

LaTeX

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

Lean4

theorem lt_map_of_nat_lt_translationNumber {n : ℕ} (h : ↑n < τ f) (x : ℝ) : x + n < f x :=
  @lt_map_of_int_lt_translationNumber f n h x

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

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

Разделы

Аффилиация

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