exists_disjoint_union_of_even_card_iff

English

For any finite set s, s has even cardinality if and only if there exist disjoint t,u with t ∪ u = s and |t| = |u|.

Русский

Для любого конечного множества s мощность чётна тогда и только тогда существует разбиение на два непересекающихся подмножества с равной мощностью.

LaTeX

$$$\\text{Even } |s| \\iff \\exists t,u:\\ (t \\cup u = s) \\land (t \\cap u = \\emptyset) \\land |t| = |u|$$$

Lean4

theorem exists_disjoint_union_of_even_card_iff [DecidableEq α] (s : Finset α) :
    Even #s ↔ ∃ (t u : Finset α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u :=
  ⟨Finset.exists_disjoint_union_of_even_card,
    by
    rintro ⟨t, u, rfl, hdtu, hctu⟩
    simp_all⟩

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