translationNumber_le_of_le_add_nat

English

Let f be a CircleDeg1Lift lift. If for every x we have f(x) ≤ x + m with m a natural number, then τ(f) ≤ m.

Русский

Пусть f — подъем гомеоморфизма окружности. Если для каждого x выполняется f(x) ≤ x + m, где m ∈ ℕ, то τ(f) ≤ m.

LaTeX

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

Lean4

theorem translationNumber_le_of_le_add_nat {x : ℝ} {m : ℕ} (h : f x ≤ x + m) : τ f ≤ m :=
  @translationNumber_le_of_le_add_int f x m h

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