English
Let t ⊆ ι' and g : ι → ι' and f : ι → N. If for all y ∉ t, ∏ x ∈ s with g x = y, f x ≤ 1, then ∏ x ∈ s f x ≤ ∏ y ∈ t ∏ x ∈ s with g x = y, f x.
Русский
Для t ⊆ ι', g : ι → ι', f : ι → N. Если для всех y ∉ t, ∏ x ∈ s с 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'} {g : \\iota \\to \\iota'} {f : \\iota \\to N}, ( \\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 sum_fiberwise_le_sum_of_sum_fiber_nonneg]
theorem prod_fiberwise_le_prod_of_one_le_prod_fiber' [MulLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N}
(h : ∀ y ∉ t, (1 : N) ≤ ∏ x ∈ s with g x = y, f x) : (∏ y ∈ t, ∏ x ∈ s with g x = y, f x) ≤ ∏ x ∈ s, f x :=
calc
(∏ y ∈ t, ∏ x ∈ s with g x = y, f x) ≤ ∏ y ∈ t ∪ s.image g, ∏ x ∈ s with g x = y, f x :=
prod_le_prod_of_subset_of_one_le' subset_union_left fun y _ ↦ h y
_ = ∏ x ∈ s, f x := prod_fiberwise_of_maps_to (fun _ hx ↦ mem_union.2 <| Or.inr <| mem_image_of_mem _ hx) _
