odd_sum_iff_odd_card_odd — Mathlib

English

For Finset s and f: ι → Nat, Odd (sum i∈s f(i)) is equivalent to Odd of the card of {x∈s | Odd(f(x))}.

Русский

Для Finset s и функции f: ι → Nat, нечётная сумма ∑ f(i) эквивалентна нечётности числа элементов x∈s, таких что f(x) нечётно.

LaTeX

$$$$ \text{Odd}\Bigl(\sum_{i \in s} f(i)\Bigr) \iff \text{Odd}\Bigl(\#\{x \in s \mid \text{Odd}(f(x))\}\Bigr). $$$$

Lean4

theorem odd_sum_iff_odd_card_odd {s : Finset ι} (f : ι → ℕ) : Odd (∑ i ∈ s, f i) ↔ Odd #({x ∈ s | Odd (f x)}) := by
  simp only [← Nat.not_even_iff_odd, even_sum_iff_even_card_odd]

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