English
Let t ⊆ ι' and g : ι → ι' and f : ι → N. If for all y ∉ t, the fiber product ∏ x ∈ s with g x = y, f x is ≤ 1, then the overall product ∏ x ∈ s f x is ≤ ∏_{y∈t} ∏_{x∈s with g x = y} f x.
Русский
Пусть t ⊆ ι', g : ι → ι', f : ι → N. Если для всех y ∉ t, волокновое произведение по x с g x = y, f x ≤ 1, тогда ∏ x∈s f x ≤ ∏_{y∈t} ∏_{x∈s с g x = y} f x.
LaTeX
$$$ \\forall \\iota\\ \\, \\iota'\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], {s : \\mathrm{Finset} \\iota} {t : \\mathrm{Finset} \\iota'} {f : \\iota \\to N} {g : \\iota \\to \\iota'}, ( \\forall y \\notin t, \\prod x \\in s with g x = y, f x \\le 1 ) \\\\Rightarrow ( \\prod_{x\\in s} f x ) \\le ( \\prod_{y\\in t} \\prod_{x\\in s with g x = y} f x ). $$$
Lean4
@[to_additive card_nsmul_le_sum]
theorem pow_card_le_prod [MulLeftMono N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) :
n ^ #s ≤ s.prod f :=
Finset.prod_le_pow_card (N := Nᵒᵈ) _ _ _ h
