le_translationNumber_of_add_int_le

English

For any f, and any x ∈ ℝ and integer m, if x + m ≤ f(x) then m ≤ τ(f).

Русский

Для любого f, для любого x ∈ ℝ и целого m, если x + m ≤ f(x), то m ≤ τ(f).

LaTeX

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

Lean4

theorem le_translationNumber_of_add_int_le {x : ℝ} {m : ℤ} (h : x + m ≤ f x) : ↑m ≤ τ f :=
  ge_of_tendsto' (f.tendsto_translation_number' x) fun n =>
    (le_div_iff₀ (n.cast_add_one_pos : (0 : ℝ) < _)).mpr <|
      le_sub_iff_add_le'.2 <| by
        simp only [coe_pow, mul_comm (m : ℝ), ← Nat.cast_add_one, f.le_iterate_of_add_int_le_map h]

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