odd_ncard_compl_iff — Mathlib

English

If |α| is even, then Odd(sᶜ.ncard) ↔ Odd(s.ncard).

Русский

Если кардинальность α чётна, то нечётность дополнения совпадает с нечётностью множества: Odd(sᶜ.ncard) ↔ Odd(s.ncard).

LaTeX

$$$$ \text{[Finite }\alpha],\; \mathrm{Even}(\mathrm{Nat.card}(\alpha)) \Rightarrow \forall s, \mathrm{Odd}((s^{c}).ncard) \Leftrightarrow \mathrm{Odd}(s.ncard) $$$$

Lean4

theorem odd_ncard_compl_iff [Finite α] (heven : Even (Nat.card α)) (s : Set α) : Odd sᶜ.ncard ↔ Odd s.ncard := by
  rw [← Nat.not_even_iff_odd, even_ncard_compl_iff heven, Nat.not_even_iff_odd]

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