Аналіз I, Глава 3.6

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

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

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

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

@[reducible, inline]

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

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

Equations

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

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

Приклад 3.6.2

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

Приклад 3.6.3

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

Твердження 3.6.4 / Вправа 3.6.1

Equations

• Chapter3.SetTheory.Set.inst_setoid = { r := Chapter3.SetTheory.Set.equal_card, 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.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.has_card_iff [SetTheory] (X : Set) (n : ℕ) : X.has_card n ↔ ∃ (f : X.toSubtype → (Fin n).toSubtype), Function.Bijective f

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 (Унікальність потужності)

@[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

@[reducible, inline]

noncomputable abbrev 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.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

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

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

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

Вправа 3.6.2

theorem Chapter3.SetTheory.Set.prod_equal_card_prod [SetTheory] (A B : Set) : (A ×ˢ B).equal_card (B ×ˢ A)

Вправа 3.6.5

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

Вправа 3.6.6

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.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

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