factorial_le

Mathlib.Data.Nat.Factorial.Basic

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

English

If m ≤ n, then m! ≤ n!.

Русский

Если m ≤ n, то m! ≤ n!.

LaTeX

$$$m \le n \Rightarrow m! \le n!$$$

Lean4

@[mono, gcongr]
theorem factorial_le {m n} (h : m ≤ n) : m ! ≤ n ! :=
  le_of_dvd (factorial_pos _) (factorial_dvd_factorial h)

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

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

Разделы

Аффилиация

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