self_le_factorial

Mathlib.Data.Nat.Factorial.Basic

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

English

For all n, n ≤ n!.

Русский

Для любого n: n ≤ n!.

LaTeX

$$$n \le n!$$$

Lean4

theorem self_le_factorial : ∀ n : ℕ, n ≤ n !
  | 0 => Nat.zero_le _
  | k + 1 => Nat.le_mul_of_pos_right _ (Nat.one_le_of_lt k.factorial_pos)

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

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

Разделы

Аффилиация

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