English
Same as above, up to additive/multiplicative variants; 1 ≤ f u for u in image g implies product bound.
Русский
То же самое с вариациями по сложению/умножению; при 1 ≤ f(u) для u∈image g получаем ограничение на произведение.
LaTeX
$$$ \\forall \\iota\\, \\iota'\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], {s : \\mathrm{Finset} \\iota} {g : \\iota \\to \\iota'} {f : \\iota' \\to N}, ( \\forall u \\in s.\\mathrm{image} g, 1 \\le f u ) \\\\Rightarrow \\prod_{u \\in s.\\mathrm{image} g} f u \\le \\prod_{u\\in s} f (g u). $$$
Lean4
@[to_additive]
theorem prod_image_le_of_one_le [MulLeftMono N] {g : ι → ι'} {f : ι' → N} (hf : ∀ u ∈ s.image g, 1 ≤ f u) :
∏ u ∈ s.image g, f u ≤ ∏ u ∈ s, f (g u) := by
rw [prod_comp f g]
refine prod_le_prod' fun a hag ↦ ?_
obtain ⟨i, hi, hig⟩ := Finset.mem_image.mp hag
apply le_self_pow (hf a hag)
rw [← Nat.pos_iff_ne_zero, card_pos]
exact ⟨i, mem_filter.mpr ⟨hi, hig⟩⟩
