prod_le_prod_fiberwise_of_prod_fiber_le_one'

English

Let g : ι → ι' and f : ι' → N. If for all u ∈ s.image g we have 1 ≤ f u, then ∏_{u ∈ s.image g} f u ≤ ∏_{u ∈ s} f(g u).

Русский

Пусть g : ι → ι' и f : ι' → N. Если для всех u ∈ s.image g верно 1 ≤ f(u), тогда ∏_{u ∈ s.image g} f(u) ≤ ∏_{u ∈ s} f(g(u)).

LaTeX

$$$ \\forall \\iota\\, \\iota'\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], {s : \\mathrm{Finset} \\iota} {g : \\iota \\to \\iota'} {f : \\iota' \\to N} (hf : \\forall u \\in s.\\mathrm{image} g, 1 \\le f u) : \\\\prod_{u \\in s.\\mathrm{image} g} f u \\le \\prod_{u \\in s} f (g u). $$$

Lean4

@[to_additive sum_le_sum_fiberwise_of_sum_fiber_nonpos]
theorem prod_le_prod_fiberwise_of_prod_fiber_le_one' [MulLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N}
    (h : ∀ y ∉ t, ∏ x ∈ s with g x = y, f x ≤ 1) : ∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ s with g x = y, f x :=
  prod_fiberwise_le_prod_of_one_le_prod_fiber' (N := Nᵒᵈ) h

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