eventually_atTop_exists_nat_between

English

For real a<b, there exist integers n between a x and b x for large x.

Русский

Для действительных a<b существуют целые числа между a x и b x при больших x.

LaTeX

$$$\forall a

Lean4

theorem eventually_atTop_exists_nat_between {a b : EReal} (h : a < b) (hb : 0 ≤ b) :
    ∀ᶠ n : ℕ in atTop, ∃ m : ℕ, a * n ≤ m ∧ m ≤ b * n :=
  match a with
  | ⊤ => (not_top_lt h).rec
  | ⊥ => by
    refine Eventually.of_forall fun n ↦ ⟨0, ?_, ?_⟩ <;> rw [Nat.cast_zero]
    · apply
        mul_nonpos_iff.2 -- Split apply and exact for a 0.5s. gain

      exact .inr ⟨bot_le, n.cast_nonneg'⟩
    · exact mul_nonneg hb n.cast_nonneg'
  | (a : ℝ) =>
    match b with
    | ⊤ => by
      refine (eventually_gt_atTop 0).mono fun n n_0 ↦ ?_
      obtain ⟨m, hm⟩ := exists_nat_ge_mul h.ne n
      exact ⟨m, hm, le_of_le_of_eq le_top (top_mul_of_pos (Nat.cast_pos'.2 n_0)).symm⟩
    | ⊥ => (not_lt_bot h).rec
    | (b : ℝ) =>
      by
      obtain ⟨x, hx⟩ :=
        eventually_atTop.1 <|
          Real.eventually_atTop_exists_nat_between (EReal.coe_lt_coe_iff.1 h) (EReal.coe_nonneg.1 hb)
      obtain ⟨n, x_n⟩ := exists_nat_ge x
      refine eventually_atTop.2 ⟨n, fun k n_k ↦ ?_⟩
      simp only [← coe_coe_eq_natCast, ← EReal.coe_mul, EReal.coe_le_coe_iff]
      exact hx k (x_n.trans (Nat.cast_le.2 n_k))

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