This file contains theorems relevant to big operators in finitely supported functions.
If 0 : ℕ is not in the support of f : ℕ →₀ ℕ then 0 < ∏ x in f.support, x ^ (f x).
0 : ℕ
f : ℕ →₀ ℕ
0 < ∏ x in f.support, x ^ (f x)