exists_union_disjoint_cardinal_eq_of_even

English

If s has even ncard, there exist t,u with t ∪ u = s, Disjoint t u, and #t = #u.

Русский

Если ncard(s) чётна, существуют t,u такие, что t ∪ u = s, Disjoint(t,u), и |t| = |u|.

LaTeX

$$$\\text{Even}(s.ncard) \\Rightarrow \\exists t,u:\\ t \\cup u = s \\land Disjoint(t,u) \\land |t| = |u|$$$

Lean4

theorem exists_union_disjoint_cardinal_eq_of_even (he : Even s.ncard) :
    ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u :=
  by
  obtain hs | hs := s.infinite_or_finite
  · exact hs.exists_union_disjoint_cardinal_eq_of_infinite
  classical
  rw [ncard_eq_toFinset_card s hs] at he
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
  use t.toSet, u.toSet
  simp [← Finset.coe_union, *]

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