English
If for every x ∈ s, f(x) ≠ 1 implies x ∈ t, then ∏_{x∈s} f(x) ≤ ∏_{x∈t} f(x).
Русский
Если для каждого x ∈ s, при этом f(x) ≠ 1 ⇒ x ∈ t, то произведение по s не больше произведения по t.
LaTeX
$$$\\forall x \\in s,\; f(x) \\neq 1 \\Rightarrow x ∈ t \\Rightarrow \\prod_{x ∈ s} f(x) ≤ \\prod_{x ∈ t} f(x)$$$
Lean4
@[to_additive sum_le_sum_of_ne_zero]
theorem prod_le_prod_of_ne_one' (h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) : ∏ x ∈ s, f x ≤ ∏ x ∈ t, f x :=
by
have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
classical
calc
∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x :=
by
rw [← prod_union, filter_union_filter_neg_eq]
exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
_ ≤ ∏ x ∈ t, f x :=
mul_le_of_le_one_of_le (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
(prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp])
