eventually_atTop_exists_nat_between

English

For real a<b with hb ≥ 0, there exists infinitely many integers m such that a n ≤ m ≤ b n for large n.

Русский

Положим a<b, hb≥0, тогда для больших n существует целое m с a n ≤ m ≤ b n.

LaTeX

$$$\forall a

Lean4

theorem eventually_atTop_exists_nat_between {a b : ℝ} (h : a < b) (hb : 0 ≤ b) :
    ∀ᶠ x : ℝ in atTop, ∃ n : ℕ, a * x ≤ n ∧ n ≤ b * x :=
  by
  filter_upwards [eventually_ge_atTop 0, Real.eventually_atTop_exists_int_between h] with x x_0 ⟨m, m_a, m_b⟩
  refine ⟨m.toNat, m_a.trans (Int.cast_le.2 m.self_le_toNat), ?_⟩
  apply le_of_eq_of_le _ (max_le m_b (mul_nonneg hb x_0))
  norm_cast
  exact Int.toNat_eq_max m

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