ascPochhammer_pos — Mathlib

English

If 0 < s in a strict ordered semiring S, then 0 < (ascPochhammer S n).eval s for all n.

Русский

Если 0 < s в строгом упорядоченном полугруппе S, то 0 < (ascPochhammer S n).eval s для всех n.

LaTeX

$$$\\forall n:\\ 0 < s \\implies 0 < (ascPochammer S n).eval s$$$

Lean4

theorem ascPochhammer_pos (n : ℕ) (s : S) (h : 0 < s) : 0 < (ascPochhammer S n).eval s := by
  induction n with
  | zero =>
    simp only [ascPochhammer_zero, eval_one]
    exact zero_lt_one
  | succ n
    ih =>
    rw [ascPochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_natCast_mul, eval_mul_X, Nat.cast_comm, ←
      mul_add]
    exact mul_pos ih (lt_of_lt_of_le h (le_add_of_nonneg_right (Nat.cast_nonneg n)))

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