tendsto_nat_floor_mul_atTop — Mathlib

English

For a≥0 and a>0, the floor of a times n divided by n grows to a in the sense that ⌊a n⌋₊ / n → a as n → ∞.

Русский

Пусть a ≥ 0 и a > 0. Тогда ⌊a n⌋₊ / n → a при n → ∞.

LaTeX

$$$$\\\\lim_{n \\to \\infty} \\\\frac{\\\\lfloor a n \\\\rfloor_{+}}{n} = a.$$$$

Lean4

theorem tendsto_nat_floor_mul_atTop {α : Type _} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α]
    [Archimedean α] (a : α) (ha : 0 < a) : Tendsto (fun (x : ℕ) => ⌊a * x⌋₊) atTop atTop :=
  Tendsto.comp tendsto_nat_floor_atTop <| Tendsto.const_mul_atTop ha tendsto_natCast_atTop_atTop

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