two_pow_mul_factorial_le_factorial_two_mul

Mathlib.Data.Nat.Factorial.Basic

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

← MathLib Explorer

English

For all n, 2^n · n! ≤ (2n)!.

Русский

Для всех n: 2^n · n! ≤ (2n)!.

LaTeX

$$2^n · n! ≤ (2n)!$$

Lean4

theorem two_pow_mul_factorial_le_factorial_two_mul (n : ℕ) : 2 ^ n * n ! ≤ (2 * n)! :=
  by
  obtain _ | n := n
  · simp
  rw [Nat.mul_comm, Nat.two_mul]
  calc
    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) := Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (le_add_left _ _) _)
    _ ≤ _ := Nat.factorial_mul_pow_le_factorial

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

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

Разделы

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

Аффилиация

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