English
Let f: α → β into an ordered ring with 0 threshold; if the number of nonpositive terms in a finite set s is even, then ∏_{x∈s} f(x) ≥ 0.
Русский
Пусть f: α → β в упорядоченной кольце; если количество элементов x∈s с f(x) ≤ 0 чётно, то ∏_{x∈s} f(x) ≥ 0.
LaTeX
$$Even (Finset.filter (fun x => f x ≤ 0) s).card → 0 ≤ ∏ x ∈ s, f x$$
Lean4
theorem prod_nonneg_of_card_nonpos_even {α β : Type*} [CommRing β] [LinearOrder β] [IsStrictOrderedRing β] {f : α → β}
[DecidablePred fun x => f x ≤ 0] {s : Finset α} (h0 : Even (s.filter fun x => f x ≤ 0).card) : 0 ≤ ∏ x ∈ s, f x :=
calc
0 ≤ ∏ x ∈ s, (if f x ≤ 0 then (-1 : β) else 1) * f x :=
Finset.prod_nonneg fun x _ => by
split_ifs with hx
· simp [hx]
linarith
_ = _ := by
rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one, Finset.prod_const,
neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
