monotone_factorial

Mathlib.Data.Nat.Factorial.BigOperators

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

English

The function n ↦ n! is monotone with respect to n; if a ≤ b then a! ≤ b!.

Русский

Функция n ↦ n! возрастает; если a ≤ b, то a! ≤ b!.

LaTeX

$$a ≤ b → a! ≤ b!$$

Lean4

theorem monotone_factorial : Monotone factorial := fun _ _ => factorial_le

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

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

Разделы

Аффилиация

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