prod_pow_pos_of_zero_notMem_support

English

If 0 ∉ f.support for f : ℕ →₀ ℕ, then 0 < ∏ x ∈ f.support x^(f x).

Русский

Если 0 не в опоре f, то произведение положительно.

LaTeX

$$$0 < \prod_{x \in f.support} x^{f(x)}.$$$

Lean4

/-- If `0 : ℕ` is not in the support of `f : ℕ →₀ ℕ` then `0 < ∏ x ∈ f.support, x ^ (f x)`. -/
theorem prod_pow_pos_of_zero_notMem_support {f : ℕ →₀ ℕ} (nhf : 0 ∉ f.support) : 0 < f.prod (· ^ ·) :=
  Nat.pos_iff_ne_zero.mpr <| Finset.prod_ne_zero_iff.mpr fun _ hf => pow_ne_zero _ fun H => by subst H; exact nhf hf

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