factorial_tendsto_atTop — Mathlib

English

As n tends to infinity, n! tends to infinity, i.e., the factorial sequence diverges to infinity.

Русский

Пусть n → ∞. Тогда n! → ∞, то есть последовательность факториалов расходится к бесконечности.

LaTeX

$$$\\\\text{Tendsto}(\\\\text{Nat}.factorial, \\\\text{atTop}, \\\\text{atTop})$$$

Lean4

theorem factorial_tendsto_atTop : Tendsto Nat.factorial atTop atTop :=
  tendsto_atTop_atTop_of_monotone (fun _ _ ↦ Nat.factorial_le) fun n ↦ ⟨n, n.self_le_factorial⟩

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