stirlingSeq'_antitone — Mathlib

English

The sequence stirlingSeq ∘ succ is decreasing; specifically, for all n ≤ m we have stirlingSeq(n+1) ≥ stirlingSeq(m+1).

Русский

Последовательность stirlingSeq ∘ succ убывает: для всех n ≤ m выполняется stirlingSeq(n+1) ≥ stirlingSeq(m+1).

LaTeX

$$$$ \forall n,m\in\mathbb{N},\ n \le m \Rightarrow \mathrm{stirlingSeq}(n+1) \ge \mathrm{stirlingSeq}(m+1). $$$$

Lean4

/-- The sequence `stirlingSeq ∘ succ` is monotone decreasing -/
theorem stirlingSeq'_antitone : Antitone (stirlingSeq ∘ succ) := fun n m h =>
  (log_le_log_iff (stirlingSeq'_pos m) (stirlingSeq'_pos n)).mp (log_stirlingSeq'_antitone h)

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