Аналіз I, Розділ 3.6: Кардинальність множин

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Потужність множини
• Скінченні та нескінченні множини
• Зв'язки з Mathlib-івськіми еквівалентами

Після цього розділу ці нотації будуть вважатися застарілими на користь їхніх еквівалентів із Mathlib.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

• (Додайте підказку тут)

@[reducible, inline]

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

Визначення 3.6.1 (Рівна потужність)

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}

Приклад 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))

Приклад 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

Твердження 3.6.4 / Вправа 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

Визначення 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

Ремарка 3.6.6

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

Приклад 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 ≠ ∅

Лема 3.6.9

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

Вправа 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)

Лема 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

Твердження 3.6.8 (Унікальність потужності)

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

Вправа 3.6.3, сформульовано з використанням натуральних чисел Mathlib

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

Теорема 3.6.12

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

Для цілей Lean зручно надавати нескінченним множинам сміттєву потужність як нуль.

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

Вправа 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

Твердження 3.6.14 (a) / Вправа 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

Твердження 3.6.14 (b) / Вправа 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

Твердження 3.6.14 (b) / Вправа 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

Твердження 3.6.14 (c) / Вправа 3.6.4

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

Твердження 3.6.14 (c) / Вправа 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

Твердження 3.6.14 (d) / Вправа 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

Твердження 3.6.14 (d) / Вправа 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

Твердження 3.6.14 (e) / Вправа 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

Твердження 3.6.14 (f) / Вправа 3.6.4

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

Вправа 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)

Вправа 3.6.6. Вам може знагодитися SetTheory.Set.curry_equiv.

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

Вправа 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

Вправа 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

Вправа 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

Вправа 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

Вправа 3.6.11

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

Вправа 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

Вправа 3.6.12 (i), перша частина

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)

Це пов'язує нашу концепцію перестановки з Mathlib-им Equiv між Fin n та 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

Будь-який Fin n можна перетворити на Fin (n + 1). Порівняйте з 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

Будь-який Fin (n + 1), крім n, можна перетворити на Fin n. Порівняйте з 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

Будь-яке натуральне число n можна перетворити на Fin (n + 1). Порівняйте з 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

Зараз хороший час, щоб довести цей результат, який буде корисним для виконання вправи 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

Якщо деякий x : Fin (n+1) ніколи не дорівнює i, ми можемо зменшити його до Fin n, зсунувши всі x > i на один вниз. Порівняйте з 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

Ми можемо розширити x : Fin n до Fin (n + 1}, зсуваючи всі x ≥ i на один вверх. Результат ніколи не дорівнює i, тому він утворює обернений процес до зменшення, виконаного predAbove. Порівняйте з 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

Вправа 3.6.12 (i), друга частина

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

Вправа 3.6.12 (ii)

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

Зв'язки іх Mathlib-ім Finite

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

Зв'язки іх Mathlib-ім Set.Finite

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

Зв'язки із Mathlib-овським Nat.card

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

Зв'язки із Mathlib-овським Set.ncard