English
If s is a finite nonempty set and f: s → α has a constant sign t, then sign(sum_{i∈s} f(i)) = t.
Русский
Если s — конечное непустое множество и f: s → α имеет постоянный знак t, то знак суммы равен t.
LaTeX
$$$\text{If } s \text{ nonempty and } \forall i \in s, \operatorname{sign}(f(i)) = t, \text{ then } \operatorname{sign}\left(\sum_{i \in s} f(i)\right) = t$$$
Lean4
theorem sign_sum {ι : Type*} {s : Finset ι} {f : ι → α} (hs : s.Nonempty) (t : SignType) (h : ∀ i ∈ s, sign (f i) = t) :
sign (∑ i ∈ s, f i) = t := by
cases t
· simp_rw [zero_eq_zero, sign_eq_zero_iff] at h ⊢
exact Finset.sum_eq_zero h
· simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢
exact Finset.sum_neg h hs
· simp_rw [pos_eq_one, sign_eq_one_iff] at h ⊢
exact Finset.sum_pos h hs
