prod_sdiff_lt_prod_sdiff — Mathlib

English

For finite sets s,t ⊆ ι and f: ι → M, we have ∏_{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) < \prod_{i \in t \setminus s} f(i) \iff \prod_{i \in s} f(i) < \prod_{i \in t} f(i)$$$

Lean4

@[to_additive]
theorem prod_sdiff_lt_prod_sdiff : ∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i :=
  by
  rw [← mul_lt_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

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