Analysis I, Section 3.6: Cardinality of sets

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Cardinality of a set
• Finite and infinite sets
• Connections with Mathlib equivalents

After this section, these notions will be deprecated in favor of their Mathlib equivalents.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

• (Add tip here)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.EqualCard [SetTheory] (X Y : Set) : Prop

Definition 3.6.1 (Equal cardinality)

Equations

• X.EqualCard Y = ∃ (f : X.toSubtype → Y.toSubtype), Function.Bijective f

theorem Chapter3.SetTheory.Set.Example_3_6_2 [SetTheory] : {0, 1, 2}.EqualCard {3, 4, 5}

Example 3.6.2

theorem Chapter3.SetTheory.Set.Example_3_6_3 [SetTheory] : nat.EqualCard (nat.specify fun (x : nat.toSubtype) => Even (nat_equiv.symm x))

Example 3.6.3

theorem Chapter3.SetTheory.Set.EqualCard.refl [SetTheory] (X : Set) : X.EqualCard X

theorem Chapter3.SetTheory.Set.EqualCard.symm [SetTheory] {X Y : Set} (h : X.EqualCard Y) : Y.EqualCard X

theorem Chapter3.SetTheory.Set.EqualCard.trans [SetTheory] {X Y Z : Set} (h1 : X.EqualCard Y) (h2 : Y.EqualCard Z) : X.EqualCard Z

instance Chapter3.SetTheory.Set.EqualCard.inst_setoid [SetTheory] : Setoid Set

Proposition 3.6.4 / Exercise 3.6.1

Equations

• Chapter3.SetTheory.Set.EqualCard.inst_setoid = { r := Chapter3.SetTheory.Set.EqualCard, iseqv := ⋯ }

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.has_card [SetTheory] (X : Set) (n : ℕ) : Prop

Definition 3.6.5

Equations

• X.has_card n = (X ≈ Chapter3.SetTheory.Set.Fin n)

theorem Chapter3.SetTheory.Set.has_card_iff [SetTheory] (X : Set) (n : ℕ) : X.has_card n ↔ ∃ (f : X.toSubtype → (Fin n).toSubtype), Function.Bijective f

theorem Chapter3.SetTheory.Set.Remark_3_6_6 [SetTheory] (n : ℕ) : (nat.specify fun (x : nat.toSubtype) => 1 ≤ nat_equiv.symm x ∧ nat_equiv.symm x ≤ n).has_card n

Remark 3.6.6

theorem Chapter3.SetTheory.Set.Example_3_6_7a [SetTheory] (a : Object) : {a}.has_card 1

Example 3.6.7

theorem Chapter3.SetTheory.Set.Example_3_6_7b [SetTheory] {a b c d : Object} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) : {a, b, c, d}.has_card 4

theorem Chapter3.SetTheory.Set.pos_card_nonempty [SetTheory] {n : ℕ} (h : n ≥ 1) {X : Set} (hX : X.has_card n) : X ≠ ∅

Lemma 3.6.9

theorem Chapter3.SetTheory.Set.has_card_zero [SetTheory] {X : Set} : X.has_card 0 ↔ X = ∅

Exercise 3.6.2a

theorem Chapter3.SetTheory.Set.card_erase [SetTheory] {n : ℕ} (h : n ≥ 1) {X : Set} (hX : X.has_card n) (x : X.toSubtype) : (X \ {↑x}).has_card (n - 1)

Lemma 3.6.9

theorem Chapter3.SetTheory.Set.card_uniq [SetTheory] {X : Set} {n m : ℕ} (h1 : X.has_card n) (h2 : X.has_card m) : n = m

Proposition 3.6.8 (Uniqueness of cardinality)

theorem Chapter3.SetTheory.Set.Example_3_6_8_a [SetTheory] : {0, 1, 2}.has_card 3

theorem Chapter3.SetTheory.Set.Example_3_6_8_b [SetTheory] : {3, 4}.has_card 2

theorem Chapter3.SetTheory.Set.Example_3_6_8_c [SetTheory] : ¬{0, 1, 2} ≈ {3, 4}

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.finite [SetTheory] (X : Set) : Prop

Equations

• X.finite = ∃ (n : ℕ), X.has_card n

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.infinite [SetTheory] (X : Set) : Prop

Equations

• X.infinite = ¬X.finite

theorem Chapter3.SetTheory.Set.bounded_on_finite [SetTheory] {n : ℕ} (f : (Fin n).toSubtype → nat.toSubtype) : ∃ (M : ℕ), ∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ M

Exercise 3.6.3, phrased using Mathlib natural numbers

theorem Chapter3.SetTheory.Set.nat_infinite [SetTheory] : nat.infinite

Theorem 3.6.12

noncomputable def Chapter3.SetTheory.Set.card [SetTheory] (X : Set) : ℕ

It is convenient for Lean purposes to give infinite sets the junk cardinality of zero.

Equations

• X.card = if h : X.finite then Exists.choose h else 0

theorem Chapter3.SetTheory.Set.has_card_card [SetTheory] {X : Set} (hX : X.finite) : X.has_card X.card

theorem Chapter3.SetTheory.Set.has_card_to_card [SetTheory] {X : Set} {n : ℕ} : X.has_card n → X.card = n

theorem Chapter3.SetTheory.Set.card_to_has_card [SetTheory] {X : Set} {n : ℕ} (hn : n ≠ 0) : X.card = n → X.has_card n

theorem Chapter3.SetTheory.Set.card_fin_eq [SetTheory] (n : ℕ) : (Fin n).has_card n

theorem Chapter3.SetTheory.Set.Fin_card [SetTheory] (n : ℕ) : (Fin n).card = n

theorem Chapter3.SetTheory.Set.Fin_finite [SetTheory] (n : ℕ) : (Fin n).finite

theorem Chapter3.SetTheory.Set.EquivCard_to_has_card_eq [SetTheory] {X Y : Set} {n : ℕ} (h : X ≈ Y) : X.has_card n ↔ Y.has_card n

theorem Chapter3.SetTheory.Set.EquivCard_to_card_eq [SetTheory] {X Y : Set} (h : X ≈ Y) : X.card = Y.card

theorem Chapter3.SetTheory.Set.empty_iff_card_eq_zero [SetTheory] {X : Set} : X = ∅ ↔ X.finite ∧ X.card = 0

Exercise 3.6.2

theorem Chapter3.SetTheory.Set.empty_of_card_eq_zero [SetTheory] {X : Set} (hX : X.finite) : X.card = 0 → X = ∅

theorem Chapter3.SetTheory.Set.finite_of_empty [SetTheory] {X : Set} : X = ∅ → X.finite

theorem Chapter3.SetTheory.Set.card_eq_zero_of_empty [SetTheory] {X : Set} : X = ∅ → X.card = 0

@[simp]

theorem Chapter3.SetTheory.Set.empty_finite [SetTheory] : ∅.finite

@[simp]

theorem Chapter3.SetTheory.Set.empty_card_eq_zero [SetTheory] : ∅.card = 0

theorem Chapter3.SetTheory.Set.card_insert [SetTheory] {X : Set} (hX : X.finite) {x : Object} (hx : x ∉ X) : (X ∪ {x}).finite ∧ (X ∪ {x}).card = X.card + 1

Proposition 3.6.14 (a) / Exercise 3.6.4

theorem Chapter3.SetTheory.Set.card_union [SetTheory] {X Y : Set} (hX : X.finite) (hY : Y.finite) : (X ∪ Y).finite ∧ (X ∪ Y).card ≤ X.card + Y.card

Proposition 3.6.14 (b) / Exercise 3.6.4

theorem Chapter3.SetTheory.Set.card_union_disjoint [SetTheory] {X Y : Set} (hX : X.finite) (hY : Y.finite) (hdisj : Disjoint X Y) : (X ∪ Y).card = X.card + Y.card

Proposition 3.6.14 (b) / Exercise 3.6.4

theorem Chapter3.SetTheory.Set.card_subset [SetTheory] {X Y : Set} (hX : X.finite) (hY : Y ⊆ X) : Y.finite ∧ Y.card ≤ X.card

Proposition 3.6.14 (c) / Exercise 3.6.4

theorem Chapter3.SetTheory.Set.card_ssubset [SetTheory] {X Y : Set} (hX : X.finite) (hY : Y ⊂ X) : Y.card < X.card

Proposition 3.6.14 (c) / Exercise 3.6.4

theorem Chapter3.SetTheory.Set.card_image [SetTheory] {X Y : Set} (hX : X.finite) (f : X.toSubtype → Y.toSubtype) : (image f X).finite ∧ (image f X).card ≤ X.card

Proposition 3.6.14 (d) / Exercise 3.6.4

theorem Chapter3.SetTheory.Set.card_image_inj [SetTheory] {X Y : Set} (hX : X.finite) {f : X.toSubtype → Y.toSubtype} (hf : Function.Injective f) : (image f X).card = X.card

Proposition 3.6.14 (d) / Exercise 3.6.4

theorem Chapter3.SetTheory.Set.card_prod [SetTheory] {X Y : Set} (hX : X.finite) (hY : Y.finite) : (X ×ˢ Y).finite ∧ (X ×ˢ Y).card = X.card * Y.card

Proposition 3.6.14 (e) / Exercise 3.6.4

noncomputable def Chapter3.SetTheory.Set.pow_fun_equiv [SetTheory] {A B : Set} : (A ^ B).toSubtype ≃ (B.toSubtype → A.toSubtype)

Equations

• Chapter3.SetTheory.Set.pow_fun_equiv = { toFun := sorry, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }

theorem Chapter3.SetTheory.Set.pow_fun_eq_iff [SetTheory] {A B : Set} (x y : (A ^ B).toSubtype) : x = y ↔ pow_fun_equiv x = pow_fun_equiv y

theorem Chapter3.SetTheory.Set.card_pow [SetTheory] {X Y : Set} (hY : Y.finite) (hX : X.finite) : (Y ^ X).finite ∧ (Y ^ X).card = Y.card ^ X.card

Proposition 3.6.14 (f) / Exercise 3.6.4

theorem Chapter3.SetTheory.Set.prod_EqualCard_prod [SetTheory] (A B : Set) : (A ×ˢ B).EqualCard (B ×ˢ A)

Exercise 3.6.5. You might find SetTheory.Set.prod_commutator useful.

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.pow_fun_equiv' [SetTheory] (A B : Set) : (A ^ B).toSubtype ≃ (B.toSubtype → A.toSubtype)

Equations

• A.pow_fun_equiv' B = Chapter3.SetTheory.Set.pow_fun_equiv

theorem Chapter3.SetTheory.Set.pow_pow_EqualCard_pow_prod [SetTheory] (A B C : Set) : ((A ^ B) ^ C).EqualCard (A ^ B ×ˢ C)

Exercise 3.6.6. You may find SetTheory.Set.curry_equiv useful.

theorem Chapter3.SetTheory.Set.pow_pow_eq_pow_mul [SetTheory] (a b c : ℕ) : (a ^ b) ^ c = a ^ (b * c)

theorem Chapter3.SetTheory.Set.pow_prod_pow_EqualCard_pow_union [SetTheory] (A B C : Set) (hd : Disjoint B C) : ((A ^ B) ×ˢ (A ^ C)).EqualCard (A ^ (B ∪ C))

theorem Chapter3.SetTheory.Set.pow_mul_pow_eq_pow_add [SetTheory] (a b c : ℕ) : a ^ b * a ^ c = a ^ (b + c)

theorem Chapter3.SetTheory.Set.injection_iff_card_le [SetTheory] {A B : Set} (hA : A.finite) (hB : B.finite) : (∃ (f : A.toSubtype → B.toSubtype), Function.Injective f) ↔ A.card ≤ B.card

Exercise 3.6.7

theorem Chapter3.SetTheory.Set.surjection_from_injection [SetTheory] {A B : Set} (hA : A ≠ ∅) (f : A.toSubtype → B.toSubtype) (hf : Function.Injective f) : ∃ (g : B.toSubtype → A.toSubtype), Function.Surjective g

Exercise 3.6.8

theorem Chapter3.SetTheory.Set.card_union_add_card_inter [SetTheory] {A B : Set} (hA : A.finite) (hB : B.finite) : A.card + B.card = (A ∪ B).card + (A ∩ B).card

Exercise 3.6.9

theorem Chapter3.SetTheory.Set.pigeonhole_principle [SetTheory] {n : ℕ} {A : (Fin n).toSubtype → Set} (hA : ∀ (i : (Fin n).toSubtype), (A i).finite) (hAcard : ((Fin n).iUnion A).card > n) : ∃ (i : (Fin n).toSubtype), (A i).card ≥ 2

Exercise 3.6.10

theorem Chapter3.SetTheory.Set.two_to_two_iff [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) : Function.Injective f ↔ ∀ S ⊆ X, S.card = 2 → (image f S).card = 2

Exercise 3.6.11

def Chapter3.SetTheory.Set.Permutations [SetTheory] (n : ℕ) : Set

Exercise 3.6.12

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter3.SetTheory.Set.Permutations_finite [SetTheory] (n : ℕ) : (Permutations n).finite

Exercise 3.6.12 (i), first part

noncomputable def Chapter3.SetTheory.Set.Permutations_toFun [SetTheory] {n : ℕ} (p : (Permutations n).toSubtype) : (Fin n).toSubtype → (Fin n).toSubtype

Equations

• Chapter3.SetTheory.Set.Permutations_toFun p = ⋯.choose

theorem Chapter3.SetTheory.Set.Permutations_bijective [SetTheory] {n : ℕ} (p : (Permutations n).toSubtype) : Function.Bijective (Permutations_toFun p)

theorem Chapter3.SetTheory.Set.Permutations_inj [SetTheory] {n : ℕ} (p1 p2 : (Permutations n).toSubtype) : Permutations_toFun p1 = Permutations_toFun p2 ↔ p1 = p2

noncomputable def Chapter3.SetTheory.Set.perm_equiv_equiv [SetTheory] {n : ℕ} : (Permutations n).toSubtype ≃ ((Fin n).toSubtype ≃ (Fin n).toSubtype)

This connects our concept of a permutation with Mathlib's Equiv between Fin n and Fin n.

Equations

• One or more equations did not get rendered due to their size.

def Chapter3.SetTheory.Set.Fin.castSucc [SetTheory] {n : ℕ} (x : (Fin n).toSubtype) : (Fin (n + 1)).toSubtype

Any Fin n can be cast to Fin (n + 1). Compare to Mathlib Fin.castSucc.

Equations

• Chapter3.SetTheory.Set.Fin.castSucc x = Chapter3.SetTheory.Set.Fin_embed n (n + 1) ⋯ x

@[simp]

theorem Chapter3.SetTheory.Set.Fin.castSucc_inj [SetTheory] {n : ℕ} {x y : (Fin n).toSubtype} : castSucc x = castSucc y ↔ x = y

@[simp]

theorem Chapter3.SetTheory.Set.Fin.castSucc_ne [SetTheory] {n : ℕ} (x : (Fin n).toSubtype) : ↑(castSucc x) ≠ n

noncomputable def Chapter3.SetTheory.Set.Fin.castPred [SetTheory] {n : ℕ} (x : (Fin (n + 1)).toSubtype) (h : ↑x ≠ n) : (Fin n).toSubtype

Any Fin (n + 1) except n can be cast to Fin n. Compare to Mathlib Fin.castPred.

Equations

• Chapter3.SetTheory.Set.Fin.castPred x h = Chapter3.SetTheory.Set.Fin_mk n ↑x ⋯

@[simp]

theorem Chapter3.SetTheory.Set.Fin.castSucc_castPred [SetTheory] {n : ℕ} (x : (Fin (n + 1)).toSubtype) (h : ↑x ≠ n) : castSucc (castPred x h) = x

@[simp]

theorem Chapter3.SetTheory.Set.Fin.castPred_castSucc [SetTheory] {n : ℕ} (x : (Fin n).toSubtype) (h : ↑(castSucc x) ≠ n) : castPred (castSucc x) h = x

def Chapter3.SetTheory.Set.Fin.last [SetTheory] (n : ℕ) : (Fin (n + 1)).toSubtype

Any natural n can be cast to Fin (n + 1). Compare to Mathlib Fin.last.

Equations

• Chapter3.SetTheory.Set.Fin.last n = Chapter3.SetTheory.Set.Fin_mk (n + 1) n ⋯

theorem Chapter3.SetTheory.Set.card_iUnion_card_disjoint [SetTheory] {n m : ℕ} {S : (Fin n).toSubtype → Set} (hSc : ∀ (i : (Fin n).toSubtype), (S i).has_card m) (hSd : Pairwise fun (i j : (Fin n).toSubtype) => Disjoint (S i) (S j)) : ((Fin n).iUnion S).finite ∧ ((Fin n).iUnion S).card = n * m

Now is a good time to prove this result, which will be useful for completing Exercise 3.6.12 (i).

noncomputable def Chapter3.SetTheory.Set.Fin.predAbove [SetTheory] {n : ℕ} (i x : (Fin (n + 1)).toSubtype) (h : x ≠ i) : (Fin n).toSubtype

If some x : Fin (n+1) is never equal to i, we can shrink it into Fin n by shifting all x > i down by one. Compare to Mathlib Fin.predAbove.

Equations

• Chapter3.SetTheory.Set.Fin.predAbove i x h = if hx : ↑x < ↑i then Chapter3.SetTheory.Set.Fin_mk n ↑x ⋯ else Chapter3.SetTheory.Set.Fin_mk n (↑x - 1) ⋯

noncomputable def Chapter3.SetTheory.Set.Fin.succAbove [SetTheory] {n : ℕ} (i : (Fin (n + 1)).toSubtype) (x : (Fin n).toSubtype) : (Fin (n + 1)).toSubtype

We can expand x : Fin n into Fin (n + 1) by shifting all x ≥ i up by one. The output is never i, so it forms an inverse to the shrinking done by predAbove. Compare to Mathlib Fin.succAbove.

Equations

• Chapter3.SetTheory.Set.Fin.succAbove i x = if ↑x < ↑i then Chapter3.SetTheory.Set.Fin_embed n (n + 1) ⋯ x else Chapter3.SetTheory.Set.Fin_mk (n + 1) (↑x + 1) ⋯

@[simp]

theorem Chapter3.SetTheory.Set.Fin.succAbove_ne [SetTheory] {n : ℕ} (i : (Fin (n + 1)).toSubtype) (x : (Fin n).toSubtype) : succAbove i x ≠ i

@[simp]

theorem Chapter3.SetTheory.Set.Fin.succAbove_predAbove [SetTheory] {n : ℕ} (i x : (Fin (n + 1)).toSubtype) (h : x ≠ i) : succAbove i (predAbove i x h) = x

@[simp]

theorem Chapter3.SetTheory.Set.Fin.predAbove_succAbove [SetTheory] {n : ℕ} (i : (Fin (n + 1)).toSubtype) (x : (Fin n).toSubtype) : predAbove i (succAbove i x) ⋯ = x

theorem Chapter3.SetTheory.Set.Permutations_ih [SetTheory] (n : ℕ) : (Permutations (n + 1)).card = (n + 1) * (Permutations n).card

Exercise 3.6.12 (i), second part

theorem Chapter3.SetTheory.Set.Permutations_card [SetTheory] (n : ℕ) : (Permutations n).card = n.factorial

Exercise 3.6.12 (ii)

theorem Chapter3.SetTheory.Set.finite_iff_finite [SetTheory] {X : Set} : X.finite ↔ Finite X.toSubtype

Connections with Mathlib's Finite

theorem Chapter3.SetTheory.Set.finite_iff_set_finite [SetTheory] {X : Set} : X.finite ↔ {x : Object | x ∈ X}.Finite

Connections with Mathlib's Set.Finite

theorem Chapter3.SetTheory.Set.card_eq_nat_card [SetTheory] {X : Set} : X.card = Nat.card X.toSubtype

Connections with Mathlib's Nat.card

theorem Chapter3.SetTheory.Set.card_eq_ncard [SetTheory] {X : Set} : X.card = {x : Object | x ∈ X}.ncard

Connections with Mathlib's Set.ncard