English
For finite sets s,t ⊆ ι and a function f: ι → M, the following are equivalent: ∏_{i∈s\t} f(i) ≤ ∏_{i∈t\s} f(i) if and only if ∏_{i∈s} f(i) ≤ ∏_{i∈t} f(i).
Русский
Для конечных множеств s,t ⊆ ι и функции f: ι → M верно: произведение по s\t не превышает произведение по t\s тогда и только тогда, когда произведение по s не превосходит произведение по t.
LaTeX
$$$\prod_{i \in s \setminus t} f(i) \le \prod_{i \in t \setminus s} f(i) \iff \prod_{i \in s} f(i) \le \prod_{i \in t} f(i)$$$
Lean4
@[to_additive]
theorem prod_sdiff_le_prod_sdiff : ∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i :=
by
rw [← mul_le_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter, ← prod_union, inter_comm,
sdiff_union_inter]
simpa only [inter_comm] using disjoint_sdiff_inter t s
