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

@[simp]

theorem finsum_one {α : Type u_1} {s : Set α} : ∑ᶠ (i : α) (_ : i ∈ s), 1 = s.ncard

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

theorem Set.Finite.ncard_biUnion {α : Type u_1} {ι : Type u_2} {t : Set ι} (ht : t.Finite) {s : ι → Set α} (hs : ∀ i ∈ t, (s i).Finite) (h : t.PairwiseDisjoint s) : (⋃ i ∈ t, s i).ncard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard

theorem Set.ncard_iUnion_of_finite {α : Type u_1} {ι : Type u_2} [Finite ι] {s : ι → Set α} (hs : ∀ (i : ι), (s i).Finite) (h : Pairwise (Function.onFun Disjoint s)) : (⋃ (i : ι), s i).ncard = ∑ᶠ (i : ι), (s i).ncard

theorem Set.Finite.encard_biUnion {α : Type u_1} {ι : Type u_2} {t : Set ι} (ht : t.Finite) {s : ι → Set α} (hs : t.PairwiseDisjoint s) : (⋃ i ∈ t, s i).encard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

theorem Set.encard_iUnion_of_finite {α : Type u_1} {ι : Type u_2} [Finite ι] {s : ι → Set α} (hs : Pairwise (Function.onFun Disjoint s)) : (⋃ (i : ι), s i).encard = ∑ᶠ (i : ι), (s i).encard