exists_union_disjoint_ncard_eq_of_even

English

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

Русский

Если ncard(M) чётна, существует разбиение на два непересекающихся подмножества с равной чисельностью элементов.

LaTeX

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

Lean4

theorem exists_union_disjoint_ncard_eq_of_even (he : Even s.ncard) :
    ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard :=
  by
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := exists_union_disjoint_cardinal_eq_of_even he
  exact ⟨t, u, hutu, hdtu, congrArg Cardinal.toNat hctu⟩

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