lt_factorial_self

Mathlib.Data.Nat.Factorial.Basic

URI: https://scilib.ai/kg/mathlib#Nat.lt_factorial_self

← MathLib Explorer

English

If hi: 3 ≤ n, then n < n!.

Русский

Если hi: 3 ≤ n, то n < n!.

LaTeX

$$$\forall {n:\mathbb{N}}, 3 \le n \rightarrow n < n!$$$

Lean4

theorem lt_factorial_self {n : ℕ} (hi : 3 ≤ n) : n < n ! :=
  by
  have : 0 < n := by omega
  have hn : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
  rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]
  exact (Nat.lt_mul_iff_one_lt_right (pred n).succ_pos).2 ((Nat.lt_of_lt_of_le hn (self_le_factorial _)))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru