choose_mono

Mathlib.Data.Nat.Choose.Basic

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

English

For every fixed b, the function a ↦ C(a,b) is monotone increasing.

Русский

Для фиксированного b функция a ↦ C(a,b) монотонно возрастает.

LaTeX

$$$$ \text{Monotone}_{a}(a \mapsto \binom{a}{b}) $$$$

Lean4

theorem choose_mono (b : ℕ) : Monotone fun a => choose a b := fun _ _ => choose_le_choose b

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

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

Разделы

Аффилиация

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