exists_disjoint_union_of_even_card

English

If a finite set s has even cardinality, then there exist disjoint subsets t and u with t ∪ u = s and |t| = |u|.

Русский

Если множество s конечное и имеет чётную мощность, то существуют попарно непересекающиеся подмножества t и u такие, что t ∪ u = s и |t| = |u|.

LaTeX

$$$\\exists t,u \\subseteq s:\\ (t \\cup u = s) \\land (t \\cap u = \\emptyset) \\land |t| = |u|$$$

Lean4

theorem exists_disjoint_union_of_even_card [DecidableEq α] {s : Finset α} (he : Even #s) :
    ∃ (t u : Finset α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u :=
  let ⟨n, hn⟩ := he
  let ⟨t, ht, ht'⟩ := exists_subset_card_eq (show n ≤ #s by cutsat)
  ⟨t, s \ t, by simp [card_sdiff_of_subset, disjoint_sdiff, *]⟩

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