Results using cardinal arithmetic

This file contains results using cardinal arithmetic that are not in the main cardinal theory files. It has been separated out to not burden Matlib.Data.Set.Card with extra imports.

Main results

• exists_union_disjoint_ncard_eq_of_even: Given a set s with an even cardinality, there exist disjoint sets t and u such that t ∪ u = s and t.ncard = u.ncard.
• exists_union_disjoint_cardinal_eq_iff is the same, except using cardinal notation.

theorem Finset.exists_disjoint_union_of_even_card {α : Type u_1} [DecidableEq α] {s : Finset α} (he : Even s.card) : ∃ (t : Finset α) (u : Finset α), t ∪ u = s ∧ Disjoint t u ∧ t.card = u.card

theorem Finset.exists_disjoint_union_of_even_card_iff {α : Type u_1} [DecidableEq α] (s : Finset α) : Even s.card ↔ ∃ (t : Finset α) (u : Finset α), t ∪ u = s ∧ Disjoint t u ∧ t.card = u.card

theorem Set.Infinite.exists_union_disjoint_cardinal_eq_of_infinite {α : Type u_1} {s : Set α} (h : s.Infinite) : ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk ↑t = Cardinal.mk ↑u

theorem Set.exists_union_disjoint_cardinal_eq_of_even {α : Type u_1} {s : Set α} (he : Even s.ncard) : ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk ↑t = Cardinal.mk ↑u

theorem Set.exists_union_disjoint_ncard_eq_of_even {α : Type u_1} {s : Set α} (he : Even s.ncard) : ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

theorem Set.exists_union_disjoint_cardinal_eq_iff {α : Type u_1} (s : Set α) : Even s.ncard ↔ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ Cardinal.mk ↑t = Cardinal.mk ↑u