descFactorial_le — Mathlib

English

For fixed n, the map k ↦ n.descFactorial k is monotone increasing in k: if k ≤ m then n.descFactorial k ≤ n.descFactorial m.

Русский

При фиксированном n отображение k ↦ n↓k неубывает по k: если k ≤ m, то n↓k ≤ n↓m.

LaTeX

$$k ≤ m → n.descFactorial k ≤ n.descFactorial m$$

Lean4

theorem descFactorial_le (n : ℕ) {k m : ℕ} (h : k ≤ m) : k.descFactorial n ≤ m.descFactorial n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [descFactorial_succ, descFactorial_succ]
    exact Nat.mul_le_mul (Nat.sub_le_sub_right h n) ih

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