tendsto_nat_ceil_atTop — Mathlib

English

The ceiling function applied to a grows without bound: ⌈x⌉₊ → ∞ as x → ∞.

Русский

Функция потолка применительно к x неограниченно растёт: ⌈x⌉₊ → ∞ при x → ∞.

LaTeX

$$$$\\\\lim_{x \\to \\infty} ⌈x⌉_{+} = \\infty.$$$$

Lean4

theorem tendsto_nat_ceil_atTop {α : Type*} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] :
    Tendsto (fun x : α ↦ ⌈x⌉₊) atTop atTop :=
  by
  refine Nat.ceil_mono.tendsto_atTop_atTop (fun x ↦ ⟨x, ?_⟩)
  simp only [Nat.ceil_natCast, le_refl]

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