even_ncard_compl_iff — Mathlib

English

If |α| is even, then parity of the complement’s cardinality equals the parity of the original set’s cardinality: Even(sᶜ.ncard) ↔ Even(s.ncard).

Русский

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

LaTeX

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

Lean4

theorem even_ncard_compl_iff [Finite α] (heven : Even (Nat.card α)) (s : Set α) : Even sᶜ.ncard ↔ Even s.ncard := by
  rwa [iff_comm, ← Nat.even_add, ncard_add_ncard_compl]

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