English
If s ⊆ t and for all i ∈ t \ s we have 1 ≤ f(i), then ∏_{i∈s} f(i) ≤ ∏_{i∈t} f(i).
Русский
Если s ⊆ t и для всех i ∈ t \\ s выполняется 1 ≤ f(i), тогда ∏_{i∈s} f(i) ≤ ∏_{i∈t} f(i).
LaTeX
$$$ \\forall \\iota\\, N\\, [\\text{CommMonoid } N], [\\text{PartialOrder } N], {f : \\iota \\to N} {s t : \\mathrm{Finset} \\iota}, s \\subseteq t \\rightarrow ( \\forall i \\in t \\setminus s, 1 \\le f(i) ) \\Rightarrow \\prod_{i \\in s} f(i) \\le \\prod_{i \\in t} f(i). $$$
Lean4
@[to_additive (attr := gcongr) sum_le_sum_of_subset_of_nonneg]
theorem prod_le_prod_of_subset_of_one_le' [MulLeftMono N] (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) :
∏ i ∈ s, f i ≤ ∏ i ∈ t, f i := by
classical
calc
∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
le_mul_of_one_le_left' <| one_le_prod' <| by simpa only [mem_sdiff, and_imp]
_ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
_ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
