factorial_lt_of_lt

Mathlib.Data.Nat.Factorial.Basic

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

English

If 0 < n and n < m, then n! < m!.

Русский

Если 0 < n и n < m, то n! < m!.

LaTeX

$$$0 < n \rightarrow n < m \rightarrow n! < m!$$$

Lean4

@[gcongr]
theorem factorial_lt_of_lt {m n : ℕ} (hn : 0 < n) (h : n < m) : n ! < m ! :=
  (factorial_lt hn).mpr h

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

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

Разделы

Аффилиация

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