tendsto_nat_ceil_div_atTop — Mathlib

English

The statement Tendsto (⌈x⌉₊ / x) atTop (nhds 1) holds under FloorRing assumptions; in particular it mirrors tendsto_floor_div_atTop.

Русский

Условия FloorRing дают, что ⌈x⌉₊ / x стремится к 1 при x → ∞.

LaTeX

$$$$\\\\lim_{x \\to \\infty} \\\\frac{\\\\lceil x \\\\rceil_{+}}{x} = 1.$$$$

Lean4

theorem tendsto_nat_ceil_div_atTop : Tendsto (fun x ↦ (⌈x⌉₊ : R) / x) atTop (𝓝 1) := by
  simpa using tendsto_nat_ceil_mul_div_atTop (zero_le_one' R)

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