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

У цій главі ми пропонуємо версію теорії множин Цермело-Франкеля (з атомами), яка намагається максимально точно наслідувати оригінальний тексту Аналізу I, Глава 3.1. Вся нумерація посилається на оригінальний текст.

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

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

• Тип множин Chapter3.SetTheory.Set

• Тип об'єктів Chapter3.SetTheory.Object

• Аксіома що кожна множина є (або може бути перетворена на) об'єкт

• Порожня множина ∅, сінглетони {y}, та пари {y,z} (та більш узагальнені кінцеві кортежі), із їх супутнімі аксіомами

• Попарне об'єднання X ∪ Y, та його супутні аксіоми

• Приведення множини A до пов'язаного з нею типу A.toSubtype, який є підтипом Object, та базового API. (Це технічна конструкція, необхідна для того, щоб зробити теорію множин Цермело-Франкеля сумісною з теорією залежних типів Lean.)

• Специфікація A.specify P множини A та предикат P: A.toSubtype → Prop до підмножини елементів A, що підпорядковуються P, та аксіома специфікації. TODO: якось реалізувати конструктора множин для цього.

• Заміна A.replace hP множини A за допомогою предиката P: A.toSubtype → Object → Prop, що підпорядковується умові унікальності ∀ x y y', P x y ∧ P x y' → y = y', та аксіомі заміщення.

• Бієктивна відповідність між натуральними числами Mathlib ℕ та множиною Chapter3.Nat : Chapter3.Set (аксіомою нескінченності).

• Аксіоми регулярності, степеневої множини та об'єднання (використовуються в наступних розділах цього розділу, але не обов'язкові тут)

• Поєднання із Mathlib-овською нотацію множини

Інші аксіоми теорії множин Цермело-Френкеля обговорюються в наступних розділах.

Деякі технічні зауваження:

• Звичайно, Mathlib має власне поняття Set, яке несумісне з поняттям Chapter3.Set, визначеним тут, хоча ми спробуємо зробити позначення максимально збігаючимися. Це спричиняє певний конфлікт позначень: наприклад, може знадобитися явно вказати (∅:Chapter3.Set) замість просто ∅, щоб вказати, що використовується версія порожньої множини Chapter3.Set, а не версія порожньої множини Mathlib, і аналогічно для інших позначень, визначених тут.
• В Аналізі I ми вирішили працювати з "нечистою" теорією множин, в якій може бути більше Object-ів, ніж просто Set-ів. У теорії типів Lean це вимагає розглядати Chapter3.Set та Chapter3.Object як окремі типи. Іноді це означає, що нам доводиться використовувати приведення X.toObject від Chapter3.Set X, щоб перетворити його на Chapter3.Object: це здебільшого потрібно під час маніпулювання множинами множин.
• Після завершення цього розділу поняття Chapter3.SetTheory.Set буде відхилено на користь стандартного позначення Set від Mathlib (або, точніше, типу Set X множини в заданому типі X). Однак, через різні технічні несумісності між теорією множин та теорією типів, ми не намагатимемося створити будь-яку еквівалентність між цими двома поняттями множин. (Таким чином, це робить весь цей розділ необов'язковим з точки зору решти книги, хоча ми зберігаємо його для педагогічних цілей.)

class Chapter3.SetTheory : Type 1

Деякі аксіоми теорії Цермело-Франкеля з атомами

• Set : Type
• Object : Type
• set_to_object : Set ↪ Object
• mem : Object → Set → Prop
• extensionality (X Y : Set) : (∀ (x : Object), mem x X ↔ mem x Y) → X = Y
• emptyset : Set
• emptyset_mem (x : Object) : ¬mem x emptyset
• singleton : Object → Set
• singleton_axiom (x y : Object) : mem x (singleton y) ↔ x = y
• union_pair : Set → Set → Set
• union_pair_axiom (X Y : Set) (x : Object) : mem x (union_pair X Y) ↔ mem x X ∨ mem x Y
• specify (A : Set) (P : { x : Object // mem x A } → Prop) : Set
• specification_axiom (A : Set) (P : { x : Object // mem x A } → Prop) : (∀ (x : Object), mem x (specify A P) → mem x A) ∧ ∀ (x : { x : Object // mem x A }), mem (↑x) (specify A P) ↔ P x
• replace (A : Set) (P : { x : Object // mem x A } → Object → Prop) (hP : ∀ (x : { x : Object // mem x A }) (y y' : Object), P x y ∧ P x y' → y = y') : Set
• replacement_axiom (A : Set) (P : { x : Object // mem x A } → Object → Prop) (hP : ∀ (x : { x : Object // mem x A }) (y y' : Object), P x y ∧ P x y' → y = y') (y : Object) : mem y (replace A P hP) ↔ ∃ (x : { x : Object // mem x A }), P x y
• nat : Set
• nat_equiv : ℕ ≃ { x : Object // mem x nat }
• regularity_axiom (A : Set) (hA : ∃ (x : Object), mem x A) : ∃ (x : Object), mem x A ∧ ∀ (S : Set), x = set_to_object S → ¬∃ (y : Object), mem y A ∧ mem y S
• pow : Set → Set → Set
• function_to_object (X Y : Set) : ({ x : Object // mem x X } → { x : Object // mem x Y }) ↪ Object
• power_set_axiom (X Y : Set) (F : Object) : mem F (pow X Y) ↔ ∃ (f : { x : Object // mem x Y } → { x : Object // mem x X }), (function_to_object Y X) f = F
• union : Set → Set
• union_axiom (A : Set) (x : Object) : mem x (union A) ↔ ∃ (S : Set), mem x S ∧ mem (set_to_object S) A

instance Chapter3.objects_mem_sets [SetTheory] : Membership Object Set

Визначення 3.1.1 (об'єкти можуть бути елементами множин)

Equations

• Chapter3.objects_mem_sets = { mem := fun (X : Chapter3.Set) (x : Chapter3.Object) => Chapter3.SetTheory.mem x X }

instance Chapter3.sets_are_objects [SetTheory] : Coe Set Object

Аксіома 3.1 (Множини це об'єкти)

Equations

• Chapter3.sets_are_objects = { coe := fun (X : Chapter3.Set) => Chapter3.SetTheory.set_to_object X }

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.toObject [SetTheory] (X : Set) : Object

Equations

• X.toObject = Chapter3.SetTheory.set_to_object X

theorem Chapter3.SetTheory.Set.coe_eq [SetTheory] {X Y : Set} (h : X.toObject = Y.toObject) : X = Y

Аксіома 3.1 (Множини це об'єкти)

@[simp]

theorem Chapter3.SetTheory.Set.coe_eq_iff [SetTheory] (X Y : Set) : X.toObject = Y.toObject ↔ X = Y

Аксіома 3.1 (Множини це об'єкти)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.ext [SetTheory] {X Y : Set} (h : ∀ (x : Object), x ∈ X ↔ x ∈ Y) : X = Y

Аксіома 3.2 (Рівність множин)

Equations

• ⋯ = ⋯

theorem Chapter3.SetTheory.Set.ext_iff [SetTheory] (X Y : Set) : X = Y ↔ ∀ (x : Object), x ∈ X ↔ x ∈ Y

Аксіома 3.2 (Рівність множин)

instance Chapter3.SetTheory.Set.instEmpty [SetTheory] : EmptyCollection Set

Equations

• Chapter3.SetTheory.Set.instEmpty = { emptyCollection := Chapter3.SetTheory.emptyset }

@[simp]

theorem Chapter3.SetTheory.Set.not_mem_empty [SetTheory] (x : Object) : x ∉ ∅

Axiom 3.3 (порожня множина). Примітка: можливо, доведеться явно перетворити ∅ на Set через існуючу нотацію теорії множин Mathlib.

theorem Chapter3.SetTheory.Set.eq_empty_iff_forall_notMem [SetTheory] {X : Set} : X = ∅ ↔ ∀ (x : Object), x ∉ X

Порожня множина не має елементів

theorem Chapter3.SetTheory.Set.empty_unique [SetTheory] : ∃! X : Set, ∀ (x : Object), x ∉ X

Порожня множина унікальна

theorem Chapter3.SetTheory.Set.nonempty_def [SetTheory] {X : Set} (h : X ≠ ∅) : ∃ (x : Object), x ∈ X

Лема 3.1.5 (Одиничний вибір)

theorem Chapter3.SetTheory.Set.nonempty_of_inhabited [SetTheory] {X : Set} {x : Object} (h : x ∈ X) : X ≠ ∅

instance Chapter3.SetTheory.Set.instSingleton [SetTheory] : Singleton Object Set

Equations

• Chapter3.SetTheory.Set.instSingleton = { singleton := Chapter3.SetTheory.singleton }

@[simp]

theorem Chapter3.SetTheory.Set.mem_singleton [SetTheory] (x a : Object) : x ∈ {a} ↔ x = a

Axiom 3.3(a) (сінглтон). Зверніть увагу, що, можливо, доведеться явно перетворити {a} на Set через існуючу нотацію теорії множин Mathlib.

instance Chapter3.SetTheory.Set.instUnion [SetTheory] : Union Set

Equations

• Chapter3.SetTheory.Set.instUnion = { union := Chapter3.SetTheory.union_pair }

@[simp]

theorem Chapter3.SetTheory.Set.mem_union [SetTheory] (x : Object) (X Y : Set) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y

Аксіома 3.4 (Попарне об'єднання)

instance Chapter3.SetTheory.Set.instInsert [SetTheory] : Insert Object Set

Equations

• Chapter3.SetTheory.Set.instInsert = { insert := fun (x : Chapter3.Object) (X : Chapter3.Set) => {x} ∪ X }

theorem Chapter3.SetTheory.Set.pair_eq [SetTheory] (a b : Object) : {a, b} = {a} ∪ {b}

Аксіома 3.3(b) (пара). Зверніть увагу, що часто доводиться перетворювати {a,b} на Set

@[simp]

theorem Chapter3.SetTheory.Set.mem_pair [SetTheory] (x a b : Object) : x ∈ {a, b} ↔ x = a ∨ x = b

Аксіома 3.3(b) (пара). Зверніть увагу, що часто доводиться перетворювати {a,b} на Set

@[simp]

theorem Chapter3.SetTheory.Set.mem_triple [SetTheory] {c : Object} (x a b : Object) : x ∈ {a, b, c} ↔ x = a ∨ x = b ∨ x = c

theorem Chapter3.SetTheory.Set.singleton_uniq [SetTheory] (a : Object) : ∃! X : Set, ∀ (x : Object), x ∈ X ↔ x = a

Ремарка 3.1.8

theorem Chapter3.SetTheory.Set.pair_uniq [SetTheory] (a b : Object) : ∃! X : Set, ∀ (x : Object), x ∈ X ↔ x = a ∨ x = b

Ремарка 3.1.8

theorem Chapter3.SetTheory.Set.pair_comm [SetTheory] (a b : Object) : {a, b} = {b, a}

Ремарка 3.1.8

theorem Chapter3.SetTheory.Set.pair_self [SetTheory] (a : Object) : {a, a} = {a}

Ремарка 3.1.8

theorem Chapter3.SetTheory.Set.pair_eq_pair [SetTheory] {a b c d : Object} (h : {a, b} = {c, d}) : a = c ∧ b = d ∨ a = d ∧ b = c

Вправа 3.1.1

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.empty [SetTheory] : Set

Equations

• Chapter3.SetTheory.Set.empty = ∅

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.singleton_empty [SetTheory] : Set

Equations

• Chapter3.SetTheory.Set.singleton_empty = {Chapter3.SetTheory.Set.empty.toObject}

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.pair_empty [SetTheory] : Set

Equations

• Chapter3.SetTheory.Set.pair_empty = {Chapter3.SetTheory.Set.empty.toObject, Chapter3.SetTheory.Set.singleton_empty.toObject}

theorem Chapter3.SetTheory.Set.emptyset_neq_singleton [SetTheory] : empty ≠ singleton_empty

Вправа 3.1.2

theorem Chapter3.SetTheory.Set.emptyset_neq_pair [SetTheory] : empty ≠ pair_empty

Вправа 3.1.2

theorem Chapter3.SetTheory.Set.singleton_empty_neq_pair [SetTheory] : singleton_empty ≠ pair_empty

Вправа 3.1.2

theorem Chapter3.SetTheory.Set.union_congr_left [SetTheory] (A A' B : Set) (h : A = A') : A ∪ B = A' ∪ B

Ремарка 3.1.11. (Ці результати можна довести або прямим переписуванням, або за допомогою екстенсіональності.)

theorem Chapter3.SetTheory.Set.union_congr_right [SetTheory] (A B B' : Set) (h : B = B') : A ∪ B = A ∪ B'

Ремарка 3.1.11. (Ці результати можна довести або прямим переписуванням, або за допомогою екстенсіональності.)

theorem Chapter3.SetTheory.Set.singleton_union_singleton [SetTheory] (a b : Object) : {a} ∪ {b} = {a, b}

Лема 3.1.12 (Основні властивості об'єднань) / Вправа 3.1.3

theorem Chapter3.SetTheory.Set.union_comm [SetTheory] (A B : Set) : A ∪ B = B ∪ A

Лема 3.1.12 (Основні властивості об'єднань) / Вправа 3.1.3

theorem Chapter3.SetTheory.Set.union_assoc [SetTheory] (A B C : Set) : A ∪ B ∪ C = A ∪ (B ∪ C)

Лема 3.1.12 (Основні властивості об'єднань) / Вправа 3.1.3

theorem Chapter3.SetTheory.Set.union_self [SetTheory] (A : Set) : A ∪ A = A

Твердження 3.1.27(c)

theorem Chapter3.SetTheory.Set.union_empty [SetTheory] (A : Set) : A ∪ ∅ = A

Твердження 3.1.27(a)

theorem Chapter3.SetTheory.Set.empty_union [SetTheory] (A : Set) : ∅ ∪ A = A

Твердження 3.1.27(a)

theorem Chapter3.SetTheory.Set.triple_eq [SetTheory] (a b c : Object) : {a, b, c} = {a} ∪ {b, c}

theorem Chapter3.SetTheory.Set.pair_union_pair [SetTheory] (a b c : Object) : {a, b} ∪ {b, c} = {a, b, c}

Приклад 3.1.10

instance Chapter3.SetTheory.Set.instSubset [SetTheory] : HasSubset Set

Визначення 3.1.14.

Equations

• Chapter3.SetTheory.Set.instSubset = { Subset := fun (X Y : Chapter3.Set) => ∀ x ∈ X, x ∈ Y }

instance Chapter3.SetTheory.Set.instSSubset [SetTheory] : HasSSubset Set

Визначення 3.1.14. Зверніть увагу, що операція строгої підмножини в Mathlib позначається ⊂, а не ⊊.

Equations

• Chapter3.SetTheory.Set.instSSubset = { SSubset := fun (X Y : Chapter3.Set) => X ⊆ Y ∧ X ≠ Y }

theorem Chapter3.SetTheory.Set.subset_def [SetTheory] (X Y : Set) : X ⊆ Y ↔ ∀ x ∈ X, x ∈ Y

Визначення 3.1.14.

theorem Chapter3.SetTheory.Set.ssubset_def [SetTheory] (X Y : Set) : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y

Визначення 3.1.14. Зверніть увагу, що операція строгої підмножини в Mathlib позначається ⊂, а не ⊊.

theorem Chapter3.SetTheory.Set.subset_congr_left [SetTheory] {A A' B : Set} (hAA' : A = A') (hAB : A ⊆ B) : A' ⊆ B

Ремарка 3.1.15

theorem Chapter3.SetTheory.Set.subset_self [SetTheory] (A : Set) : A ⊆ A

Приклади 3.1.16

theorem Chapter3.SetTheory.Set.empty_subset [SetTheory] (A : Set) : ∅ ⊆ A

Приклади 3.1.16

theorem Chapter3.SetTheory.Set.subset_trans [SetTheory] {A B C : Set} (hAB : A ⊆ B) (hBC : B ⊆ C) : A ⊆ C

Твердження 3.1.17 (Часткове впорядкування через підмножини)

theorem Chapter3.SetTheory.Set.subset_antisymm [SetTheory] (A B : Set) (hAB : A ⊆ B) (hBA : B ⊆ A) : A = B

Твердження 3.1.17 (Часткове впорядкування через підмножини)

theorem Chapter3.SetTheory.Set.ssubset_trans [SetTheory] (A B C : Set) (hAB : A ⊂ B) (hBC : B ⊂ C) : A ⊂ C

Твердження 3.1.17 (Часткове впорядкування через підмножини)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.toSubtype [SetTheory] (A : Set) : Type

This defines the subtype A.toSubtype for any A:Set. To produce an element x' of this subtype, use ⟨ x, hx ⟩, where x:Object and hx:x ∈ A. The object x associated to a subtype element x' is recovered as x.val, and the property hx that x belongs to A is recovered as x.property Це визначає підтип A.toSubtype для будь-якого A:Set. Щоб створити елемент x' цього підтипу, використовуйте ⟨ x, hx ⟩, де x:Object та hx:x ∈ A. Об'єкт x, пов'язаний з елементом підтипу x', відновлюється як x.val, а властивість hx, що x належить A, відновлюється як x.property.

Equations

• A.toSubtype = { x : Chapter3.Object // x ∈ A }

instance Chapter3.instCoeSortSetType [SetTheory] : CoeSort Set Type

Equations

• Chapter3.instCoeSortSetType = { coe := fun (A : Chapter3.Set) => A.toSubtype }

theorem Chapter3.SetTheory.Set.subtype_property [SetTheory] (A : Set) (x : A.toSubtype) : ↑x ∈ A

Елементи множини (неявно приведені до підтипу) також є елементами множини (щодо операції належності теорії множин).

theorem Chapter3.SetTheory.Set.subtype_coe [SetTheory] (A : Set) (x : A.toSubtype) : ↑x = ↑x

theorem Chapter3.SetTheory.Set.coe_inj [SetTheory] (A : Set) (x y : A.toSubtype) : ↑x = ↑y ↔ x = y

def Chapter3.SetTheory.Set.subtype_mk [SetTheory] (A : Set) {x : Object} (hx : x ∈ A) : A.toSubtype

Якщо є доказ hx для x ∈ A, тоді A.subtype_mk hx зробить елемент A (розглядаємий як підтип) відповідним x.

Equations

• A.subtype_mk hx = ⟨x, hx⟩

theorem Chapter3.SetTheory.Set.subtype_mk_coe [SetTheory] {A : Set} {x : Object} (hx : x ∈ A) : ↑(A.subtype_mk hx) = x

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.specify [SetTheory] (A : Set) (P : A.toSubtype → Prop) : Set

Equations

• A.specify P = Chapter3.SetTheory.specify A P

theorem Chapter3.SetTheory.Set.specification_axiom [SetTheory] {A : Set} {P : A.toSubtype → Prop} {x : Object} (h : x ∈ A.specify P) : x ∈ A

Аксіома 3.6 (аксіома виділення)

theorem Chapter3.SetTheory.Set.specification_axiom' [SetTheory] {A : Set} (P : A.toSubtype → Prop) (x : A.toSubtype) : ↑x ∈ A.specify P ↔ P x

Аксіома 3.6 (аксіома виділення)

theorem Chapter3.SetTheory.Set.specification_axiom'' [SetTheory] {A : Set} (P : A.toSubtype → Prop) (x : Object) : x ∈ A.specify P ↔ ∃ (h : x ∈ A), P ⟨x, h⟩

Аксіома 3.6 (аксіома виділення)

theorem Chapter3.SetTheory.Set.specify_subset [SetTheory] {A : Set} (P : A.toSubtype → Prop) : A.specify P ⊆ A

theorem Chapter3.SetTheory.Set.specify_congr [SetTheory] {A A' : Set} (hAA' : A = A') {P : A.toSubtype → Prop} {P' : A'.toSubtype → Prop} (hPP' : ∀ (x : Object) (h : x ∈ A) (h' : x ∈ A'), P ⟨x, h⟩ ↔ P' ⟨x, h'⟩) : A.specify P = A'.specify P'

Ця вправа може вимагати певного розуміння того, як підтипи реалізовані в Lean.

instance Chapter3.SetTheory.Set.instIntersection [SetTheory] : Inter Set

Equations

• Chapter3.SetTheory.Set.instIntersection = { inter := fun (X Y : Chapter3.Set) => X.specify fun (x : X.toSubtype) => ↑x ∈ Y }

@[simp]

theorem Chapter3.SetTheory.Set.mem_inter [SetTheory] (x : Object) (X Y : Set) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y

Визначення 3.1.22 (Перетин)

instance Chapter3.SetTheory.Set.instSDiff [SetTheory] : SDiff Set

Equations

• Chapter3.SetTheory.Set.instSDiff = { sdiff := fun (X Y : Chapter3.Set) => X.specify fun (x : X.toSubtype) => ↑x ∉ Y }

@[simp]

theorem Chapter3.SetTheory.Set.mem_sdiff [SetTheory] (x : Object) (X Y : Set) : x ∈ X \ Y ↔ x ∈ X ∧ x ∉ Y

Визначення 3.1.26 (Різниця)

theorem Chapter3.SetTheory.Set.inter_comm [SetTheory] (A B : Set) : A ∩ B = B ∩ A

Твердження 3.1.27(d) / Вправа 3.1.6

theorem Chapter3.SetTheory.Set.subset_union [SetTheory] {A X : Set} (hAX : A ⊆ X) : A ∪ X = X

Твердження 3.1.27(b)

theorem Chapter3.SetTheory.Set.union_subset [SetTheory] {A X : Set} (hAX : A ⊆ X) : X ∪ A = X

Твердження 3.1.27(b)

theorem Chapter3.SetTheory.Set.inter_self [SetTheory] (A : Set) : A ∩ A = A

Твердження 3.1.27(c)

theorem Chapter3.SetTheory.Set.inter_assoc [SetTheory] (A B C : Set) : A ∩ B ∩ C = A ∩ (B ∩ C)

Твердження 3.1.27(e)

theorem Chapter3.SetTheory.Set.inter_union_distrib_left [SetTheory] (A B C : Set) : A ∩ (B ∪ C) = A ∩ B ∪ A ∩ C

Твердження 3.1.27(f)

theorem Chapter3.SetTheory.Set.union_inter_distrib_left [SetTheory] (A B C : Set) : A ∪ B ∩ C = (A ∪ B) ∩ (A ∪ C)

Твердження 3.1.27(f)

theorem Chapter3.SetTheory.Set.union_compl [SetTheory] {A X : Set} (hAX : A ⊆ X) : A ∪ X \ A = X

Твердження 3.1.27(f)

theorem Chapter3.SetTheory.Set.inter_compl [SetTheory] {A X : Set} (hAX : A ⊆ X) : A ∩ (X \ A) = ∅

Твердження 3.1.27(f)

theorem Chapter3.SetTheory.Set.compl_union [SetTheory] {A B X : Set} (hAX : A ⊆ X) (hBX : B ⊆ X) : X \ (A ∪ B) = X \ A ∩ (X \ B)

Твердження 3.1.27(g)

theorem Chapter3.SetTheory.Set.compl_inter [SetTheory] {A B X : Set} (hAX : A ⊆ X) (hBX : B ⊆ X) : X \ (A ∩ B) = X \ A ∪ X \ B

Твердження 3.1.27(g)

instance Chapter3.SetTheory.Set.instDistribLattice [SetTheory] : DistribLattice Set

Не з підручника: множини утворюють дистрибутивну решітку.

Equations

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

instance Chapter3.SetTheory.Set.instOrderBot [SetTheory] : OrderBot Set

Множини мають мінімальний елемент.

Equations

• Chapter3.SetTheory.Set.instOrderBot = { bot := ∅, bot_le := ⋯ }

theorem Chapter3.SetTheory.Set.disjoint_iff [SetTheory] (A B : Set) : Disjoint A B ↔ A ∩ B = ∅

Визначення неперетинності (з використанням попередніх прикладів)

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.replace [SetTheory] (A : Set) {P : A.toSubtype → Object → Prop} (hP : ∀ (x : A.toSubtype) (y y' : Object), P x y ∧ P x y' → y = y') : Set

Equations

• A.replace hP = Chapter3.SetTheory.replace A P hP

theorem Chapter3.SetTheory.Set.replacement_axiom [SetTheory] {A : Set} {P : A.toSubtype → Object → Prop} (hP : ∀ (x : A.toSubtype) (y y' : Object), P x y ∧ P x y' → y = y') (y : Object) : y ∈ A.replace hP ↔ ∃ (x : A.toSubtype), P x y

Аксіома 3.7 (Аксіомна схема підстановки)

@[reducible, inline]

abbrev Chapter3.Nat [SetTheory] : Set

Equations

• Chapter3.Nat = Chapter3.SetTheory.nat

def Chapter3.SetTheory.Set.nat_equiv [SetTheory] : ℕ ≃ Nat.toSubtype

Аксіома 3.8 (Аксіома нескінченності)

Equations

• Chapter3.SetTheory.Set.nat_equiv = Chapter3.SetTheory.nat_equiv

instance Chapter3.SetTheory.Set.instOfNat [SetTheory] {n : ℕ} : OfNat Nat.toSubtype n

Equations

• Chapter3.SetTheory.Set.instOfNat = { ofNat := Chapter3.SetTheory.Set.nat_equiv n }

instance Chapter3.SetTheory.Set.instNatCast [SetTheory] : NatCast Nat.toSubtype

Equations

• Chapter3.SetTheory.Set.instNatCast = { natCast := fun (n : ℕ) => Chapter3.SetTheory.Set.nat_equiv n }

instance Chapter3.SetTheory.Set.toNat [SetTheory] : Coe Nat.toSubtype ℕ

Equations

• Chapter3.SetTheory.Set.toNat = { coe := fun (n : Chapter3.Nat.toSubtype) => Chapter3.SetTheory.Set.nat_equiv.symm n }

instance Chapter3.SetTheory.Object.instNatCast [SetTheory] : NatCast Object

Equations

• Chapter3.SetTheory.Object.instNatCast = { natCast := fun (n : ℕ) => ↑↑n }

instance Chapter3.SetTheory.Object.instOfNat [SetTheory] {n : ℕ} : OfNat Object n

Equations

• Chapter3.SetTheory.Object.instOfNat = { ofNat := ↑↑n }

@[simp]

theorem Chapter3.SetTheory.Object.ofnat_eq [SetTheory] {n : ℕ} : ↑↑n = ↑n

theorem Chapter3.SetTheory.Object.ofnat_eq' [SetTheory] {n : ℕ} : OfNat.ofNat n = ↑n

theorem Chapter3.SetTheory.Set.nat_coe_eq [SetTheory] {n : ℕ} : ↑n = OfNat.ofNat n

@[simp]

theorem Chapter3.SetTheory.Set.nat_equiv_inj [SetTheory] (n m : ℕ) : ↑n = ↑m ↔ n = m

@[simp]

theorem Chapter3.SetTheory.Set.nat_equiv_symm_inj [SetTheory] (n m : Nat.toSubtype) : nat_equiv.symm n = nat_equiv.symm m ↔ n = m

@[simp]

theorem Chapter3.SetTheory.Set.ofNat_inj [SetTheory] (n m : ℕ) : OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m

@[simp]

theorem Chapter3.SetTheory.Set.ofNat_inj' [SetTheory] (n m : ℕ) : OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m

@[simp]

theorem Chapter3.SetTheory.Object.natCast_inj [SetTheory] (n m : ℕ) : ↑n = ↑m ↔ n = m

@[simp]

theorem Chapter3.SetTheory.Set.nat_equiv_coe_of_coe [SetTheory] (n : ℕ) : nat_equiv.symm ↑n = n

@[simp]

theorem Chapter3.SetTheory.Set.nat_equiv_coe_of_coe' [SetTheory] (n : Nat.toSubtype) : ↑(nat_equiv.symm n) = n

theorem Chapter3.SetTheory.Set.subset_tfae [SetTheory] (A B C : Set) : [A ⊆ B, A ∪ B = B, A ∩ B = A].TFAE

Вправа 3.1.5. Тут можна використовувати тактики tfae_have та tfae_finish.

theorem Chapter3.SetTheory.Set.inter_subset_left [SetTheory] (A B : Set) : A ∩ B ⊆ A

Вправа 3.1.7

theorem Chapter3.SetTheory.Set.inter_subset_right [SetTheory] (A B : Set) : A ∩ B ⊆ B

Вправа 3.1.7

theorem Chapter3.SetTheory.Set.subset_inter_iff [SetTheory] (A B C : Set) : C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B

Вправа 3.1.7

theorem Chapter3.SetTheory.Set.subset_union_left [SetTheory] (A B : Set) : A ⊆ A ∪ B

Вправа 3.1.7

theorem Chapter3.SetTheory.Set.subset_union_right [SetTheory] (A B : Set) : B ⊆ A ∪ B

Вправа 3.1.7

theorem Chapter3.SetTheory.Set.union_subset_iff [SetTheory] (A B C : Set) : A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C

Вправа 3.1.7

theorem Chapter3.SetTheory.Set.inter_union_cancel [SetTheory] (A B : Set) : A ∩ (A ∪ B) = A

Вправа 3.1.8

theorem Chapter3.SetTheory.Set.union_inter_cancel [SetTheory] (A B : Set) : A ∪ A ∩ B = A

Вправа 3.1.8

theorem Chapter3.SetTheory.Set.partition_left [SetTheory] {A B X : Set} (h_union : A ∪ B = X) (h_inter : A ∩ B = ∅) : A = X \ B

Вправа 3.1.9

theorem Chapter3.SetTheory.Set.partition_right [SetTheory] {A B X : Set} (h_union : A ∪ B = X) (h_inter : A ∩ B = ∅) : B = X \ A

Вправа 3.1.9

theorem Chapter3.SetTheory.Set.pairwise_disjoint [SetTheory] (A B : Set) : Pairwise (Function.onFun Disjoint ![A \ B, A ∩ B, B \ A])

Вправа 3.1.10

theorem Chapter3.SetTheory.Set.union_eq_partition [SetTheory] (A B : Set) : A ∪ B = A \ B ∪ A ∩ B ∪ B \ A

Вправа 3.1.10

theorem Chapter3.SetTheory.Set.specification_from_replacement [SetTheory] {A : Set} {P : A.toSubtype → Prop} : ∃ B ⊆ A, ∀ (x : A.toSubtype), ↑x ∈ B ↔ P x

Вправа 3.1.11. Завдання полягає в тому, щоб довести це без використання Set.specify, Set.specification_axiom або Set.specification_axiom.

theorem Chapter3.SetTheory.Set.subset_union_subset [SetTheory] {A B A' B' : Set} (hA'A : A' ⊆ A) (hB'B : B' ⊆ B) : A' ∪ B' ⊆ A ∪ B

Вправа 3.1.12.

theorem Chapter3.SetTheory.Set.subset_inter_subset [SetTheory] {A B A' B' : Set} (hA'A : A' ⊆ A) (hB'B : B' ⊆ B) : A' ∩ B' ⊆ A ∩ B

Вправа 3.1.12.

theorem Chapter3.SetTheory.Set.subset_diff_subset_counter [SetTheory] : ∃ (A : Set) (B : Set) (A' : Set) (B' : Set), A' ⊆ A ∧ B' ⊆ B ∧ ¬A' \ B' ⊆ A \ B

Вправа 3.1.12.

theorem Chapter3.SetTheory.Set.singleton_iff [SetTheory] (A : Set) (hA : A ≠ ∅) : (¬∃ B ⊂ A, B ≠ ∅) ↔ ∃ (x : Object), A = {x}

Вправа 3.1.13

instance Chapter3.SetTheory.Set.inst_coe_set [SetTheory] : Coe Set (_root_.Set Object)

Equations

• Chapter3.SetTheory.Set.inst_coe_set = { coe := fun (X : Chapter3.Set) => {x : Chapter3.Object | x ∈ X} }

@[simp]

theorem Chapter3.SetTheory.Set.coe_inj' [SetTheory] (X Y : Set) : {x : Object | x ∈ X} = {x : Object | x ∈ Y} ↔ X = Y

Ін'єктивність перетворення. Зауважте, однак, що ми НЕ стверджуємо, що перетворення є сюръєктивним (і насправді парадокс Рассела цьому перешкоджає).

theorem Chapter3.SetTheory.Set.mem_coe [SetTheory] (X : Set) (x : Object) : x ∈ {x : Object | x ∈ X} ↔ x ∈ X

Сумісність операції належності ∈

theorem Chapter3.SetTheory.Set.coe_empty [SetTheory] : {x : Object | x ∈ ∅} = ∅

Сумісність порожньої множини

theorem Chapter3.SetTheory.Set.coe_subset [SetTheory] (X Y : Set) : {x : Object | x ∈ X} ⊆ {x : Object | x ∈ Y} ↔ X ⊆ Y

Сумісність підмножини

theorem Chapter3.SetTheory.Set.coe_ssubset [SetTheory] (X Y : Set) : {x : Object | x ∈ X} ⊂ {x : Object | x ∈ Y} ↔ X ⊂ Y

theorem Chapter3.SetTheory.Set.coe_singleton [SetTheory] (x : Object) : {x} = {x}

Сумісність синглтона

theorem Chapter3.SetTheory.Set.coe_union [SetTheory] (X Y : Set) : {x : Object | x ∈ X} ∪ {x : Object | x ∈ Y} = {x : Object | x ∈ X} ∪ {x : Object | x ∈ Y}

Сумісність об'еднання

theorem Chapter3.SetTheory.Set.coe_pair [SetTheory] (x y : Object) : {x, y} = {x, y}

Сумісність пари

theorem Chapter3.SetTheory.Set.coe_subtype [SetTheory] (X : Set) : ↑{x : Object | x ∈ X} = X.toSubtype

Сумісність підтипу

theorem Chapter3.SetTheory.Set.coe_intersection [SetTheory] (X Y : Set) : {x : Object | x ∈ X} ∩ {x : Object | x ∈ Y} = {x : Object | x ∈ X} ∩ {x : Object | x ∈ Y}

Сумісність перетину

theorem Chapter3.SetTheory.Set.coe_diff [SetTheory] (X Y : Set) : {x : Object | x ∈ X} \ {x : Object | x ∈ Y} = {x : Object | x ∈ X} \ {x : Object | x ∈ Y}

Сумісність різниці множин

theorem Chapter3.SetTheory.Set.coe_Disjoint [SetTheory] (X Y : Set) : Disjoint {x : Object | x ∈ X} {x : Object | x ∈ Y} ↔ Disjoint X Y

Сумісність неперетинності