Основи теорії множин

Аналіз I, Розділ 3.1: Основи теорії множин

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

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

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

Тип множин Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.SetTheory.Set
Тип об'єктів Chapter3.SetTheory.Object.{u, v} [self : Chapter3.SetTheory] : Type vChapter3.SetTheory.Object
Аксіома що кожна множина є (або може бути перетворена на) об'єкт
Порожня множина ∅ : ?m.1∅, сінглетони overloaded, errors 1:1 Unknown identifier `y` invalid {...} notation, expected type is not known{y}, та пари overloaded, errors 1:1 Unknown identifier `y` invalid {...} notation, expected type is not known{y,z} (та більш узагальнені кінцеві кортежі), із їх супутнімі аксіомами
Попарне об'єднання Unknown identifier `X`sorry ∪ sorry : ?m.1X ∪ Unknown identifier `Y`Y, та його супутні аксіоми
Приведення множини Unknown identifier `A`A до пов'язаного з нею типу Unknown identifier `A.toSubtype`A.toSubtype, який є підтипом Unknown identifier `Object`Object, та базового API. (Це технічна конструкція, необхідна для того, щоб зробити теорію множин Цермело-Франкеля сумісною з теорією залежних типів Lean.)
Специфікація Unknown identifier `A.specify`A.specify P множини Unknown identifier `A`A та предикат до підмножини елементів Unknown identifier `A`A, що підпорядковуються Unknown identifier `P`P, та аксіома специфікації. TODO: якось реалізувати конструктора множин для цього.
Заміна Unknown identifier `A.replace`A.replace hP множини Unknown identifier `A`A за допомогою предиката , що підпорядковується умові унікальності ∀ (x : ?m.1) (y y' : ?m.6 x), sorry ∧ sorry → y = y' : Prop∀ x y y', Unknown identifier `P`P x y ∧ Unknown identifier `P`P x y' → y = y', та аксіомі заміщення.
Бієктивна відповідність між натуральними числами Mathlib ℕ : Typeℕ та множиною (аксіомою нескінченності).
Аксіоми регулярності, степеневої множини та об'єднання (використовуються в наступних розділах цього розділу, але не обов'язкові тут)
Поєднання із Mathlib-овською нотацію множини

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

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

Звичайно, Mathlib має власне поняття Set.{u} (α : Type u) : Type uSet, яке несумісне з поняттям Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.Set, визначеним тут, хоча ми спробуємо зробити позначення максимально збігаючимися. Це спричиняє певний конфлікт позначень: наприклад, може знадобитися явно вказати (∅:failed to synthesize Chapter3.SetTheory Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.Chapter3.Set) замість просто ∅ : ?m.1∅, щоб вказати, що використовується версія порожньої множини Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.Set, а не версія порожньої множини Mathlib, і аналогічно для інших позначень, визначених тут.
В Аналізі I ми вирішили працювати з "нечистою" теорією множин, в якій може бути більше Unknown identifier `Object`Object-ів, ніж просто Set.{u} (α : Type u) : Type uSet-ів. У теорії типів Lean це вимагає розглядати Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.Set та Chapter3.SetTheory.Object.{u, v} [self : Chapter3.SetTheory] : Type vChapter3.Object як окремі типи. Іноді це означає, що нам доводиться використовувати приведення Unknown identifier `X.toObject`X.toObject від Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.Set Unknown identifier `X`X, щоб перетворити його на Chapter3.SetTheory.Object.{u, v} [self : Chapter3.SetTheory] : Type vChapter3.Object: це здебільшого потрібно під час маніпулювання множинами множин.
Strictly speaking, a set is not a type; however, we will coerce sets to types, and specifically to a subtype of Unknown identifier `Object`Object. A similar coercion is in place for Mathlib's formalization of sets.
Після завершення цього розділу поняття Chapter3.SetTheory.Set.{u, v} [self : Chapter3.SetTheory] : Type uChapter3.SetTheory.Set буде відхилено на користь стандартного позначення Set.{u} (α : Type u) : Type uSet від Mathlib (або, точніше, типу Set sorry : Type u_1Set Unknown identifier `X`X множини в заданому типі Unknown identifier `X`X). Однак, через різні технічні несумісності між теорією множин та теорією типів, ми не намагатимемося створити будь-яку еквівалентність між цими двома поняттями множин. (Таким чином, це робить весь цей розділ необов'язковим з точки зору решти книги, хоча ми зберігаємо його для педагогічних цілей.)

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

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

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

namespace Chapter3

/- Можливість працювати в кількох універсах наразі не є суттєвою, але стає важливою під час
   побудови моделей теорії множин в епілозі Розділу 3. -/
universe u v

Аксиоми теорії Zermelo-Frankel з атомами.

class SetTheory where
  Set : Type u -- Аксіома 3.1
  Object : Type v -- Аксіома 3.1
  set_to_object : Set ↪ Object -- Аксіома 3.1
  mem : Object → Set → Prop -- Аксіома 3.1
  extensionality X Y : (∀ x, mem x X ↔ mem x Y) → X = Y -- Аксіома 3.2
  emptyset: Set -- Аксіома 3.3
  emptyset_mem x : ¬ mem x emptyset -- Аксіома 3.3
  singleton : Object → Set -- Аксіома 3.4
  singleton_axiom x y : mem x (singleton y) ↔ x = y -- Аксіома 3.4
  union_pair : Set → Set → Set -- Аксіома 3.5
  union_pair_axiom X Y x : mem x (union_pair X Y) ↔ (mem x X ∨ mem x Y) -- Аксіома 3.5
  specify A (P: Subtype (mem .A) → Prop) : Set -- Аксіома 3.6
  specification_axiom A (P: Subtype (mem .A) → Prop) :
    (∀ x, mem x (specify A P) → mem x A) ∧ ∀ x, mem x.val (specify A P) ↔ P x -- Аксіома 3.6
  replace A (P: Subtype (mem .A) → Object → Prop)
    (hP: ∀ x y y', P x y ∧ P x y' → y = y') : Set -- Аксіома 3.7
  replacement_axiom A (P: Subtype (mem .A) → Object → Prop)
    (hP: ∀ x y y', P x y ∧ P x y' → y = y') : ∀ y, mem y (replace A P hP) ↔ ∃ x, P x y -- Аксіома 3.7
  nat : Set -- Аксіома 3.8
  nat_equiv : ℕ ≃ Subtype (mem .nat) -- Аксіома 3.8
  regularity_axiom A (hA : ∃ x, mem x A) :
    ∃ x, mem x A ∧ ∀ S, x = set_to_object S → ¬ ∃ y, mem y A ∧ mem y S -- Аксіома 3.9
  pow : Set → Set → Set -- Аксіома 3.11
  function_to_object (X: Set) (Y: Set) :
    (Subtype (mem .X) → Subtype (mem .Y)) ↪ Object -- Аксіома 3.11
  powerset_axiom (X: Set) (Y: Set) (F:Object) :
    mem F (pow X Y) ↔ ∃ f: Subtype (mem .Y) → Subtype (mem .X),
    function_to_object Y X f = F -- Аксіома 3.11
  union : Set → Set -- Аксіома 3.12
  union_axiom A x : mem x (union A) ↔ ∃ S, mem x S ∧ mem (set_to_object S) A -- Аксіома 3.12

-- Ця дозволяє використовувати `Set` та `Object` замість `SetTheory.Set` і `SetTheory.Object`.
export SetTheory (Set Object)

-- Цей екземпляр неявно нав'язує аксіоми теорії множин Цермело-Френкеля з атомами.
variable [SetTheory]

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

instance SetTheory.objects_mem_sets : Membership Object Set where
  mem X x := mem x X

-- Тепер можна використовувати оператор `∈` між нашим `Object` і `Set`.
example (X: Set) (x: Object) : x ∈ X ↔ SetTheory.mem x X := byinst✝:SetTheoryX:Setx:Object⊢ x ∈ X ↔ SetTheory.mem x X rflAll goals completed! 🐙

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

instance SetTheory.sets_are_objects : Coe Set Object where
  coe X := set_to_object X

-- Тепер ми можемо розглядати `Set` як `Object`, коли це потрібно.
example (X: Set) : (X: Object) = SetTheory.set_to_object X := rfl

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

theorem SetTheory.Set.coe_eq {X Y:Set} (h: (X: Object) = (Y: Object)) : X = Y :=
  set_to_object.inj' h

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

@[simp]
theorem SetTheory.Set.coe_eq_iff (X Y:Set) : (X: Object) = (Y: Object) ↔  X = Y :=
  ⟨ coe_eq, byinst✝:SetTheoryX:SetY:Set⊢ X = Y → set_to_object X = set_to_object Y rintro rflinst✝:SetTheoryX:Set⊢ set_to_object X = set_to_object X; rflAll goals completed! 🐙 ⟩

Аксіома 3.2 (Рівність множин). [sorry] : List ?m.2[Unknown identifier `ext`ext] тег дозволяє тактиці Unknown identifier `ext`ext працювати для множин.

@[ext]
theorem SetTheory.Set.ext {X Y:Set} (h: ∀ x, x ∈ X ↔ x ∈ Y) : X = Y := extensionality _ _ h

Chapter3.SetTheory.Set.ext_iff.{u_1, u_2} [SetTheory] {X Y : Set} : X = Y ↔ ∀ (x : Object), x ∈ X ↔ x ∈ Y

instance SetTheory.Set.instEmpty : EmptyCollection Set where
  emptyCollection := emptyset

-- Тепер ми можемо використовувати нотацію `∅` для вказання на `SetTheory.emptyset`.
example : ∅ = SetTheory.emptyset := rfl

-- Зробіть все, що ми визначаємо в `SetTheory.Set.*` доступним безпосередньо.
open SetTheory.Set

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

@[simp]
theorem SetTheory.Set.not_mem_empty : ∀ x, x ∉ (∅:Set) := emptyset_mem

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

theorem declaration uses 'sorry'SetTheory.Set.eq_empty_iff_forall_notMem {X:Set} : X = ∅ ↔ (∀ x, x ∉ X) := byinst✝:SetTheoryX:Set⊢ X = ∅ ↔ ∀ (x : Object), x ∉ X
  sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.empty_unique : ∃! (X:Set), ∀ x, x ∉ X := byinst✝:SetTheory⊢ ∃! X, ∀ (x : Object), x ∉ X
  sorryAll goals completed! 🐙

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

lemma SetTheory.Set.nonempty_def {X:Set} (h: X ≠ ∅) : ∃ x, x ∈ X := byinst✝:SetTheoryX:Seth:X ≠ ∅⊢ ∃ x, x ∈ X
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  by_contra! thisinst✝:SetTheoryX:Seth:X ≠ ∅this:∀ (x : Object), x ∉ X⊢ False
  have claim (x:Object) : x ∈ X ↔ x ∈ (∅:Set) := byinst✝:SetTheoryX:Seth:X ≠ ∅⊢ ∃ x, x ∈ X simp [this, not_mem_empty]All goals completed! 🐙
  apply ext at claiminst✝:SetTheoryX:Seth:X ≠ ∅this:∀ (x : Object), x ∉ Xclaim:X = ∅⊢ False
  contradictionAll goals completed! 🐙

theorem SetTheory.Set.nonempty_of_inhabited {X:Set} {x:Object} (h:x ∈ X) : X ≠ ∅ := byinst✝:SetTheoryX:Setx:Objecth:x ∈ X⊢ X ≠ ∅
  contrapose! hinst✝:SetTheoryX:Setx:Objecth:X = ∅⊢ x ∉ X
  rw [eq_empty_iff_forall_notMem] at hinst✝:SetTheoryX:Setx:Objecth:∀ (x : Object), x ∉ X⊢ x ∉ X
  exact h xAll goals completed! 🐙

instance SetTheory.Set.instSingleton : Singleton Object Set where
  singleton := singleton

-- Тепер ми можемо використовувати нотацію `{x}` для однієї одиниці `Set`.
example (x: Object) : {x} = SetTheory.singleton x := rfl

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

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

instance SetTheory.Set.instUnion : Union Set where
  union := union_pair

-- Тепер ми можемо використовувати нотацію `X ∪ Y` для об’єднання двох `Set`-ів.
example (X Y: Set) : X ∪ Y = SetTheory.union_pair X Y := rfl

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

@[simp]
theorem SetTheory.Set.mem_union (x:Object) (X Y:Set) : x ∈ (X ∪ Y) ↔ (x ∈ X ∨ x ∈ Y) :=
  union_pair_axiom X Y x

instance SetTheory.Set.instInsert : Insert Object Set where
  insert x X := {x} ∪ X

@[simp]
theorem SetTheory.Set.mem_insert (a b: Object) (X: Set) : a ∈ insert b X ↔ a = b ∨ a ∈ X := byinst✝:SetTheorya:Objectb:ObjectX:Set⊢ a ∈ insert b X ↔ a = b ∨ a ∈ X
  simp [instInsert]All goals completed! 🐙

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

theorem SetTheory.Set.pair_eq (a b:Object) : ({a,b}:Set) = {a} ∪ {b} := byinst✝:SetTheorya:Objectb:Object⊢ {a, b} = {a} ∪ {b} rflAll goals completed! 🐙

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

@[simp]
theorem SetTheory.Set.mem_pair (x a b:Object) : x ∈ ({a,b}:Set) ↔ (x = a ∨ x = b) := byinst✝:SetTheoryx:Objecta:Objectb:Object⊢ x ∈ {a, b} ↔ x = a ∨ x = b
  simp [pair_eq, mem_union, mem_singleton]All goals completed! 🐙

@[simp]
theorem SetTheory.Set.mem_triple (x a b c:Object) : x ∈ ({a,b,c}:Set) ↔ (x = a ∨ x = b ∨ x = c) := byinst✝:SetTheoryx:Objecta:Objectb:Objectc:Object⊢ x ∈ {a, b, c} ↔ x = a ∨ x = b ∨ x = c
  simp [Insert.insert, mem_union, mem_singleton]All goals completed! 🐙

Ремарка 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.singleton_uniq (a:Object) : ∃! (X:Set), ∀ x, x ∈ X ↔ x = a := byinst✝:SetTheorya:Object⊢ ∃! X, ∀ (x : Object), x ∈ X ↔ x = a sorryAll goals completed! 🐙

Ремарка 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.pair_uniq (a b:Object) : ∃! (X:Set), ∀ x, x ∈ X ↔ x = a ∨ x = b := byinst✝:SetTheorya:Objectb:Object⊢ ∃! X, ∀ (x : Object), x ∈ X ↔ x = a ∨ x = b sorryAll goals completed! 🐙

Ремарка 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.pair_comm (a b:Object) : ({a,b}:Set) = {b,a} := byinst✝:SetTheorya:Objectb:Object⊢ {a, b} = {b, a} sorryAll goals completed! 🐙

Ремарка 3.1.9

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.pair_self (a:Object) : ({a,a}:Set) = {a} := byinst✝:SetTheorya:Object⊢ {a, a} = {a}
  sorryAll goals completed! 🐙

Вправа 3.1.1

theorem declaration uses 'sorry'SetTheory.Set.pair_eq_pair {a b c d:Object} (h: ({a,b}:Set) = {c,d}) :
    a = c ∧ b = d ∨ a = d ∧ b = c := byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecth:{a, b} = {c, d}⊢ a = c ∧ b = d ∨ a = d ∧ b = c
  sorryAll goals completed! 🐙

abbrev SetTheory.Set.empty : Set := ∅abbrev SetTheory.Set.singleton_empty : Set := {(empty: Object)}abbrev SetTheory.Set.pair_empty : Set := {(empty: Object), (singleton_empty: Object)}

Вправа 3.1.2

theorem declaration uses 'sorry'SetTheory.Set.emptyset_neq_singleton : empty ≠ singleton_empty := byinst✝:SetTheory⊢ empty ≠ singleton_empty
  sorryAll goals completed! 🐙

Вправа 3.1.2

theorem declaration uses 'sorry'SetTheory.Set.emptyset_neq_pair : empty ≠ pair_empty := byinst✝:SetTheory⊢ empty ≠ pair_empty sorryAll goals completed! 🐙

Вправа 3.1.2

theorem declaration uses 'sorry'SetTheory.Set.singleton_empty_neq_pair : singleton_empty ≠ pair_empty := byinst✝:SetTheory⊢ singleton_empty ≠ pair_empty
  sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_congr_left (A A' B:Set) (h: A = A') : A ∪ B = A' ∪ B := byinst✝:SetTheoryA:SetA':SetB:Seth:A = A'⊢ A ∪ B = A' ∪ B sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_congr_right (A B B':Set) (h: B = B') : A ∪ B = A ∪ B' := byinst✝:SetTheoryA:SetB:SetB':Seth:B = B'⊢ A ∪ B = A ∪ B' sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.singleton_union_singleton (a b:Object) :
    ({a}:Set) ∪ ({b}:Set) = {a,b} := byinst✝:SetTheorya:Objectb:Object⊢ {a} ∪ {b} = {a, b}
  sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_comm (A B:Set) : A ∪ B = B ∪ A := byinst✝:SetTheoryA:SetB:Set⊢ A ∪ B = B ∪ A sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_assoc (A B C:Set) : (A ∪ B) ∪ C = A ∪ (B ∪ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∪ C = A ∪ (B ∪ C)
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  ext xhinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ B ∪ C ↔ x ∈ A ∪ (B ∪ C)
  constructorh.mpinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ B ∪ C → x ∈ A ∪ (B ∪ C)h.mprinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ (B ∪ C) → x ∈ A ∪ B ∪ C
  .h.mpinst✝:SetTheoryA:SetB:SetC:Setx:Object⊢ x ∈ A ∪ B ∪ C → x ∈ A ∪ (B ∪ C) intro hxh.mpinst✝:SetTheoryA:SetB:SetC:Setx:Objecthx:x ∈ A ∪ B ∪ C⊢ x ∈ A ∪ (B ∪ C); rw [mem_union] at hxh.mpinst✝:SetTheoryA:SetB:SetC:Setx:Objecthx:x ∈ A ∪ B ∨ x ∈ C⊢ x ∈ A ∪ (B ∪ C)
    obtain case1 | case2 := hxh.mp.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1:x ∈ A ∪ B⊢ x ∈ A ∪ (B ∪ C)h.mp.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase2:x ∈ C⊢ x ∈ A ∪ (B ∪ C)
    .h.mp.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1:x ∈ A ∪ B⊢ x ∈ A ∪ (B ∪ C) rw [mem_union] at case1h.mp.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1:x ∈ A ∨ x ∈ B⊢ x ∈ A ∪ (B ∪ C)
      obtain case1a | case1b := case1h.mp.inl.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1a:x ∈ A⊢ x ∈ A ∪ (B ∪ C)h.mp.inl.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1b:x ∈ B⊢ x ∈ A ∪ (B ∪ C)
      .h.mp.inl.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1a:x ∈ A⊢ x ∈ A ∪ (B ∪ C) rw [mem_union]h.mp.inl.inlinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1a:x ∈ A⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙
      have : x ∈ B ∪ C := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∪ C = A ∪ (B ∪ C) rw [mem_union]inst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1b:x ∈ B⊢ x ∈ B ∨ x ∈ C; tautoAll goals completed! 🐙
      rw [mem_union]h.mp.inl.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase1b:x ∈ Bthis:_fvar.11059 ∈ _fvar.11031 ∪ _fvar.11032 := ?_mvar.11638⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙
    have : x ∈ B ∪ C := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∪ C = A ∪ (B ∪ C) rw [mem_union]inst✝:SetTheoryA:SetB:SetC:Setx:Objectcase2:x ∈ C⊢ x ∈ B ∨ x ∈ C; tautoAll goals completed! 🐙
    rw [mem_union]h.mp.inrinst✝:SetTheoryA:SetB:SetC:Setx:Objectcase2:x ∈ Cthis:_fvar.11059 ∈ _fvar.11031 ∪ _fvar.11032 := ?_mvar.12309⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙
  sorryAll goals completed! 🐙

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

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.union_self (A:Set) : A ∪ A = A := byinst✝:SetTheoryA:Set⊢ A ∪ A = A
  sorryAll goals completed! 🐙

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

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.union_empty (A:Set) : A ∪ ∅ = A := byinst✝:SetTheoryA:Set⊢ A ∪ ∅ = A
  sorryAll goals completed! 🐙

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

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.empty_union (A:Set) : ∅ ∪ A = A := byinst✝:SetTheoryA:Set⊢ ∅ ∪ A = A
  sorryAll goals completed! 🐙

theorem SetTheory.Set.triple_eq (a b c:Object) : {a,b,c} = ({a}:Set) ∪ {b,c} := byinst✝:SetTheorya:Objectb:Objectc:Object⊢ {a, b, c} = {a} ∪ {b, c}
  rflAll goals completed! 🐙

Приклад 3.1.10

theorem SetTheory.Set.pair_union_pair (a b c:Object) :
    ({a,b}:Set) ∪ {b,c} = {a,b,c} := byinst✝:SetTheorya:Objectb:Objectc:Object⊢ {a, b} ∪ {b, c} = {a, b, c}
  exthinst✝:SetTheorya:Objectb:Objectc:Objectx✝:Object⊢ x✝ ∈ {a, b} ∪ {b, c} ↔ x✝ ∈ {a, b, c}; simp only [mem_union, mem_pair, mem_triple]hinst✝:SetTheorya:Objectb:Objectc:Objectx✝:Object⊢ (x✝ = a ∨ x✝ = b) ∨ x✝ = b ∨ x✝ = c ↔ x✝ = a ∨ x✝ = b ∨ x✝ = c; tautoAll goals completed! 🐙

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

instance SetTheory.Set.instSubset : HasSubset Set where
  Subset X Y := ∀ x, x ∈ X → x ∈ Y

-- Тепер ми можемо використовувати нотацію `⊆` для відношення підмножини між двома `Set`-ами.
example (X Y: Set) : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y := byinst✝:SetTheoryX:SetY:Set⊢ X ⊆ Y ↔ ∀ x ∈ X, x ∈ Y rflAll goals completed! 🐙

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

instance SetTheory.Set.instSSubset : HasSSubset Set where
  SSubset X Y := X ⊆ Y ∧ X ≠ Y

-- Тепер ми можемо використовувати нотацію `⊂` для відношення строгої підмножини між двома `Set`-ами.
example (X Y: Set) : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y := byinst✝:SetTheoryX:SetY:Set⊢ X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y rflAll goals completed! 🐙

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

theorem SetTheory.Set.subset_def (X Y:Set) : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y := byinst✝:SetTheoryX:SetY:Set⊢ X ⊆ Y ↔ ∀ x ∈ X, x ∈ Y rflAll goals completed! 🐙

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

theorem SetTheory.Set.ssubset_def (X Y:Set) : X ⊂ Y ↔ (X ⊆ Y ∧ X ≠ Y) := byinst✝:SetTheoryX:SetY:Set⊢ X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y rflAll goals completed! 🐙

Ремарка 3.1.15

theorem declaration uses 'sorry'SetTheory.Set.subset_congr_left {A A' B:Set} (hAA':A = A') (hAB: A ⊆ B) : A' ⊆ B := byinst✝:SetTheoryA:SetA':SetB:SethAA':A = A'hAB:A ⊆ B⊢ A' ⊆ B sorryAll goals completed! 🐙

Приклади 3.1.16

@[simp, refl]
theorem declaration uses 'sorry'SetTheory.Set.subset_self (A:Set) : A ⊆ A := byinst✝:SetTheoryA:Set⊢ A ⊆ A sorryAll goals completed! 🐙

Приклади 3.1.16

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.empty_subset (A:Set) : ∅ ⊆ A := byinst✝:SetTheoryA:Set⊢ ∅ ⊆ A sorryAll goals completed! 🐙

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

theorem SetTheory.Set.subset_trans {A B C:Set} (hAB:A ⊆ B) (hBC:B ⊆ C) : A ⊆ C := byinst✝:SetTheoryA:SetB:SetC:SethAB:A ⊆ BhBC:B ⊆ C⊢ A ⊆ C
  -- Цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  rw [subset_def]inst✝:SetTheoryA:SetB:SetC:SethAB:A ⊆ BhBC:B ⊆ C⊢ ∀ x ∈ A, x ∈ C
  intro x hxinst✝:SetTheoryA:SetB:SetC:SethAB:A ⊆ BhBC:B ⊆ Cx:Objecthx:x ∈ A⊢ x ∈ C
  rw [subset_def] at hABinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ A⊢ x ∈ C
  apply hAB x at hxinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ B⊢ x ∈ C
  apply hBC x at hxinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ C⊢ x ∈ C
  assumptionAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.subset_antisymm (A B:Set) (hAB:A ⊆ B) (hBA:B ⊆ A) : A = B := byinst✝:SetTheoryA:SetB:SethAB:A ⊆ BhBA:B ⊆ A⊢ A = B
  sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.ssubset_trans (A B C:Set) (hAB:A ⊂ B) (hBC:B ⊂ C) : A ⊂ C := byinst✝:SetTheoryA:SetB:SetC:SethAB:A ⊂ BhBC:B ⊂ C⊢ A ⊂ C
  sorryAll goals completed! 🐙

Це визначає підтип Unknown identifier `A.toSubtype`A.toSubtype для будь-якого . Зауважте, що Unknown identifier `A.toSubtype`A.toSubtype задає тип, подібно до того, як Chapter3.SetTheory.Object.{u, v} [self : SetTheory] : Type vObject або Chapter3.SetTheory.Set.{u, v} [self : SetTheory] : Type uSet є типами. Значення Unknown identifier `x'`x' типу Unknown identifier `A.toSubtype`A.toSubtype поєднує деякий із доведенням .

Щоб створити елемент Unknown identifier `x'`x' цього підтипу, використовуйте Invalid `⟨...⟩` notation: The expected type of this term could not be determined⟨ x, hx ⟩, де , а . Об’єкт Unknown identifier `x`x, пов’язаний з елементом підтипу Unknown identifier `x'`x', відновлюється як Unknown identifier `x'.val`x'.val, а властивість Unknown identifier `hx`hx, що Unknown identifier `x`x належить Unknown identifier `A`A, відновлюється як Unknown identifier `x'.property`x'.property.

abbrev SetTheory.Set.toSubtype (A:Set) := Subtype (fun x ↦ x ∈ A)

example (A: Set) (x: Object) (hx: x ∈ A) : A.toSubtype := ⟨x, hx⟩example (A: Set) (x': A.toSubtype) : Object := x'.valexample (A: Set) (x': A.toSubtype) : x'.val ∈ A := x'.property

-- В практиці, підтип дозволяє нам носити об'єкт з доказом належності як одну величину.
-- Порівняйте ці два докази. Вони еквівалентні, але остання версія покладає на себе `x` і `hx` в `x'`.
example (A B: Set) (x: Object) (hx: x ∈ A) : x ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A ∨ x ∈ B; lefthinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A; exact hxAll goals completed! 🐙

example (A B: Set) (x': A.toSubtype) : x'.val ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∨ ↑x' ∈ B; lefthinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A; exact x'.propertyAll goals completed! 🐙

instance : CoeSort (Set) (Type v) where
  coe A := A.toSubtype

-- Тепер замість написання `x': A.toSubtype`, ми можемо просто написати `x': A`.
-- Порівняйте ці три доведення. Вони еквівалентні, але останнє читається лаконічніше.
example (A B: Set) (x: Object) (hx: x ∈ A) : x ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A ∨ x ∈ B; lefthinst✝:SetTheoryA:SetB:Setx:Objecthx:x ∈ A⊢ x ∈ A; exact hxAll goals completed! 🐙

example (A B: Set) (x': A.toSubtype) : x'.val ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∨ ↑x' ∈ B; lefthinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A; exact x'.propertyAll goals completed! 🐙

example (A B: Set) (x': A) : x'.val ∈ A ∪ B := byinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∪ B simpinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A ∨ ↑x' ∈ B; lefthinst✝:SetTheoryA:SetB:Setx':A.toSubtype⊢ ↑x' ∈ A; exact x'.propertyAll goals completed! 🐙

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

lemma SetTheory.Set.subtype_property (A:Set) (x:A) : x.val ∈ A := x.property

lemma SetTheory.Set.subtype_coe (A:Set) (x:A) : x.val = x := rfllemma SetTheory.Set.coe_inj (A:Set) (x y:A) : x.val = y.val ↔ x = y := Subtype.coe_inj

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

def SetTheory.Set.subtype_mk (A:Set) {x:Object} (hx:x ∈ A) : A := ⟨ x, hx ⟩

@[simp]
lemma SetTheory.Set.subtype_mk_coe {A:Set} {x:Object} (hx:x ∈ A) : A.subtype_mk hx = x := byinst✝:SetTheoryA:Setx:Objecthx:x ∈ A⊢ ↑(A.subtype_mk hx) = x rflAll goals completed! 🐙

abbrev SetTheory.Set.specify (A:Set) (P: A → Prop) : Set := SetTheory.specify A P

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

theorem SetTheory.Set.specification_axiom {A:Set} {P: A → Prop} {x:Object} (h: x ∈ A.specify P) :
    x ∈ A :=
  (SetTheory.specification_axiom A P).1 x h

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

theorem SetTheory.Set.specification_axiom' {A:Set} (P: A → Prop) (x:A) :
    x.val ∈ A.specify P ↔ P x :=
  (SetTheory.specification_axiom A P).2 x

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

@[simp]
theorem SetTheory.Set.specification_axiom'' {A:Set} (P: A → Prop) (x:Object) :
    x ∈ A.specify P ↔ ∃ h:x ∈ A, P ⟨ x, h ⟩ := byinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Object⊢ x ∈ A.specify P ↔ ∃ (h : x ∈ A), P ⟨x, h⟩
  constructormpinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Object⊢ x ∈ A.specify P → ∃ (h : x ∈ A), P ⟨x, h⟩mprinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Object⊢ (∃ (h : x ∈ A), P ⟨x, h⟩) → x ∈ A.specify P
  .mpinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Object⊢ x ∈ A.specify P → ∃ (h : x ∈ A), P ⟨x, h⟩ intro hmpinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ A.specify P⊢ ∃ (h : x ∈ A), P ⟨x, h⟩; use specification_axiom hhinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ A.specify P⊢ P ⟨x, ⋯⟩
    simp [←specification_axiom' P, h]All goals completed! 🐙
  intro ⟨ h, hP ⟩mprinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ AhP:P ⟨x, h⟩⊢ x ∈ A.specify P
  simpa [←specification_axiom' P] using hPAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.specify_subset {A:Set} (P: A → Prop) : A.specify P ⊆ A := byinst✝:SetTheoryA:SetP:A.toSubtype → Prop⊢ A.specify P ⊆ A sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.specify_congr {A A':Set} (hAA':A = A') {P: A → Prop} {P': A' → Prop}
  (hPP': (x:Object) → (h:x ∈ A) → (h':x ∈ A') → P ⟨ x, h⟩ ↔ P' ⟨ x, h'⟩ ) :
    A.specify P = A'.specify P' := byinst✝:SetTheoryA:SetA':SethAA':A = A'P:A.toSubtype → PropP':A'.toSubtype → ProphPP':∀ (x : Object) (h : x ∈ A) (h' : x ∈ A'), P ⟨x, h⟩ ↔ P' ⟨x, h'⟩⊢ A.specify P = A'.specify P' sorryAll goals completed! 🐙

instance SetTheory.Set.instIntersection : Inter Set where
  inter X Y := X.specify (fun x ↦ x.val ∈ Y)

-- Тепер ми можемо використовувати нотацію `X ∩ Y` для перетину двох `Set`-ів.
example (X Y: Set) : X ∩ Y = X.specify (fun x ↦ x.val ∈ Y) := rfl

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

@[simp]
theorem SetTheory.Set.mem_inter (x:Object) (X Y:Set) : x ∈ (X ∩ Y) ↔ (x ∈ X ∧ x ∈ Y) := byinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y
  constructormpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∩ Y → x ∈ X ∧ x ∈ Ymprinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∧ x ∈ Y → x ∈ X ∩ Y
  .mpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∩ Y → x ∈ X ∧ x ∈ Y intro hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Y⊢ x ∈ X ∧ x ∈ Y; have h' := specification_axiom hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Yh':?_mvar.29648 := Chapter3.SetTheory.Set.specification_axiom _fvar.29644⊢ x ∈ X ∧ x ∈ Y; simp [h']mpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Yh':?_mvar.29648 := Chapter3.SetTheory.Set.specification_axiom _fvar.29644⊢ x ∈ Y
    exact (specification_axiom' _ ⟨ x, h' ⟩).mp hAll goals completed! 🐙
  intro ⟨ hX, hY ⟩mprinst✝:SetTheoryx:ObjectX:SetY:SethX:x ∈ XhY:x ∈ Y⊢ x ∈ X ∩ Y; exact (specification_axiom' (fun x ↦ x.val ∈ Y) ⟨ x,hX⟩).mpr hYAll goals completed! 🐙

instance SetTheory.Set.instSDiff : SDiff Set where
  sdiff X Y := X.specify (fun x ↦ x.val ∉ Y)

-- Тепер ми можемо використовувати нотацію `X ∩ Y` для різниці `Set`-ів.
example (X Y: Set) : X \ Y = X.specify (fun x ↦ x.val ∉ Y) := rfl

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

@[simp]
theorem SetTheory.Set.mem_sdiff (x:Object) (X Y:Set) : x ∈ (X \ Y) ↔ (x ∈ X ∧ x ∉ Y) := byinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X \ Y ↔ x ∈ X ∧ x ∉ Y
  constructormpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X \ Y → x ∈ X ∧ x ∉ Ymprinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X ∧ x ∉ Y → x ∈ X \ Y
  .mpinst✝:SetTheoryx:ObjectX:SetY:Set⊢ x ∈ X \ Y → x ∈ X ∧ x ∉ Y intro hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Y⊢ x ∈ X ∧ x ∉ Y; have h' := specification_axiom hmpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Yh':?_mvar.30370 := Chapter3.SetTheory.Set.specification_axiom _fvar.30366⊢ x ∈ X ∧ x ∉ Y; simp [h']mpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Yh':?_mvar.30370 := Chapter3.SetTheory.Set.specification_axiom _fvar.30366⊢ x ∉ Y
    exact (specification_axiom' _ ⟨ x, h' ⟩ ).mp hAll goals completed! 🐙
  intro ⟨ hX, hY ⟩mprinst✝:SetTheoryx:ObjectX:SetY:SethX:x ∈ XhY:x ∉ Y⊢ x ∈ X \ Y; exact (specification_axiom' (fun x ↦ x.val ∉ Y) ⟨ x, hX⟩ ).mpr hYAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.inter_comm (A B:Set) : A ∩ B = B ∩ A := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ B = B ∩ A sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.subset_union {A X: Set} (hAX: A ⊆ X) : A ∪ X = X := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ A ∪ X = X sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_subset {A X: Set} (hAX: A ⊆ X) : X ∪ A = X := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ X ∪ A = X sorryAll goals completed! 🐙

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

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.inter_self (A:Set) : A ∩ A = A := byinst✝:SetTheoryA:Set⊢ A ∩ A = A
  sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.inter_assoc (A B C:Set) : (A ∩ B) ∩ C = A ∩ (B ∩ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∩ B ∩ C = A ∩ (B ∩ C) sorryAll goals completed! 🐙

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

theorem  declaration uses 'sorry'SetTheory.Set.inter_union_distrib_left (A B C:Set) :
    A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∩ (B ∪ C) = A ∩ B ∪ A ∩ C
  sorryAll goals completed! 🐙

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

theorem  declaration uses 'sorry'SetTheory.Set.union_inter_distrib_left (A B C:Set) :
    A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ∩ C = (A ∪ B) ∩ (A ∪ C)
  sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_compl {A X:Set} (hAX: A ⊆ X) : A ∪ (X \ A) = X := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ A ∪ X \ A = X sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.inter_compl {A X:Set} : A ∩ (X \ A) = ∅ := byinst✝:SetTheoryA:SetX:Set⊢ A ∩ (X \ A) = ∅ sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.compl_union {A B X:Set} : X \ (A ∪ B) = (X \ A) ∩ (X \ B) := byinst✝:SetTheoryA:SetB:SetX:Set⊢ X \ (A ∪ B) = X \ A ∩ (X \ B) sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.compl_inter {A B X:Set} : X \ (A ∩ B) = (X \ A) ∪ (X \ B) := byinst✝:SetTheoryA:SetB:SetX:Set⊢ X \ (A ∩ B) = X \ A ∪ X \ B sorryAll goals completed! 🐙

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

instance declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.instDistribLattice : DistribLattice Set where
  le := (·⊆ ·)
  le_refl := subset_self
  le_trans := fun _ _ _ ↦ subset_trans
  le_antisymm := subset_antisymm
  inf := (·∩ ·)
  sup := (·∪ ·)
  le_sup_left := byinst✝:SetTheory⊢ ∀ (a b : Set), a ⊆ a ∪ b sorryAll goals completed! 🐙
  le_sup_right := byinst✝:SetTheory⊢ ∀ (a b : Set), b ⊆ a ∪ b sorryAll goals completed! 🐙
  sup_le := byinst✝:SetTheory⊢ ∀ (a b c : Set), a ⊆ c → b ⊆ c → a ∪ b ⊆ c sorryAll goals completed! 🐙
  inf_le_left := byinst✝:SetTheory⊢ ∀ (a b : Set), a ∩ b ⊆ a sorryAll goals completed! 🐙
  inf_le_right := byinst✝:SetTheory⊢ ∀ (a b : Set), a ∩ b ⊆ b sorryAll goals completed! 🐙
  le_inf := byinst✝:SetTheory⊢ ∀ (a b c : Set), a ⊆ b → a ⊆ c → a ⊆ b ∩ c sorryAll goals completed! 🐙
  le_sup_inf := byinst✝:SetTheory⊢ ∀ (x y z : Set), (x ⊔ y) ⊓ (x ⊔ z) ⊆ x ⊔ y ⊓ z
    intro X Y Zinst✝:SetTheoryX:SetY:SetZ:Set⊢ (X ⊔ Y) ⊓ (X ⊔ Z) ⊆ X ⊔ Y ⊓ Z; change (X ∪ Y) ∩ (X ∪ Z) ⊆ X ∪ (Y ∩ Z)inst✝:SetTheoryX:SetY:SetZ:Set⊢ (X ∪ Y) ∩ (X ∪ Z) ⊆ X ∪ Y ∩ Z
    rw [←union_inter_distrib_left]All goals completed! 🐙

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

instance SetTheory.Set.instOrderBot : OrderBot Set where
  bot := ∅
  bot_le := empty_subset

-- Тепер ми визначили `A ≤ B` як `A ⊆ B`, і `⊥` як `∅`.
-- Це дозволяє визначенню `Disjoint` з Mathlib працювати з нашим `Set`.
example (A B: Set) : (A ≤ B) ↔ (A ⊆ B) := byinst✝:SetTheoryA:SetB:Set⊢ A ≤ B ↔ A ⊆ B rflAll goals completed! 🐙

example : ⊥ = (∅: Set) := byinst✝:SetTheory⊢ ⊥ = ∅ rflAll goals completed! 🐙example (A B: Set) : Prop := Disjoint A B

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

theorem SetTheory.Set.disjoint_iff (A B:Set) : Disjoint A B ↔ A ∩ B = ∅ := byinst✝:SetTheoryA:SetB:Set⊢ Disjoint A B ↔ A ∩ B = ∅
  convert _root_.disjoint_iffAll goals completed! 🐙

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

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

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

abbrev Nat := SetTheory.nat

-- Надалі ми використовуватимемо `Nat` як тип.
-- Проте зауважте, що ми встановили `Nat` як `SetTheory.nat`, який є `Set`, а не типом.
-- Єдина причина, чому ми можемо писати `x: Nat`, полягає в тому, що раніше ми визначили приведення `CoeSort`,
-- яке дозволяє записувати `x: A` (коли `A` є `Set`) як скорочення для `x: A.toSubtype`.
-- Саме тому, коли ви бачите `x: Nat`, насправді мається на увазі `x: Nat.toSubtype`.
example (x: Nat) : Nat.toSubtype := x

example (x: Nat) : Object := x.valexample (x: Nat) : (x.val ∈ Nat) := x.propertyexample (o: Object) (ho: o ∈ Nat) : Nat := ⟨o, ho⟩

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

def SetTheory.Set.nat_equiv : ℕ ≃ Nat := SetTheory.nat_equiv

-- Нижче наведено деякі API для обробки приведень. Це може бути не оптимальним способом налаштування.

instance SetTheory.Set.instOfNat {n:ℕ} : OfNat Nat n where
  ofNat := nat_equiv n

-- Тепер ми можемо визначити `Nat` за допомогою натурального літерала.
example : Nat := 5

example : (5 : Nat).val ∈ Nat := (5 : Nat).property

instance SetTheory.Set.instNatCast : NatCast Nat where
  natCast n := nat_equiv n

-- Тепер ми можемо перетворити `ℕ` на `Nat`.
example (n : ℕ) : Nat := n

example (n : ℕ) : (n : Nat).val ∈ Nat := (n : Nat).property

instance SetTheory.Set.toNat : Coe Nat ℕ where
  coe n := nat_equiv.symm n

-- Тепер ми можемо перетворити `Nat` на `ℕ`.
example (n : Nat) : ℕ := n

instance SetTheory.Object.instNatCast : NatCast Object where
  natCast n := (n:Nat).val

-- Тепер ми можемо перетворити `Nat` на `Object`.
example (n: ℕ) : Object := n

example (n: ℕ) : Set := {(n: Object)}

instance SetTheory.Object.instOfNat {n:ℕ} : OfNat Object n where
  ofNat := ((n:Nat):Object)

-- Тепер ми можемо визначити `Object` за допомогою літерала натурального числа.
example : Object := 1

example : Set := {1, 2, 3}

@[simp]
lemma SetTheory.Object.ofnat_eq {n:ℕ} : ((n:Nat):Object) = (n:Object) := rfl

lemma SetTheory.Object.ofnat_eq' {n:ℕ} : (ofNat(n):Object) = (n:Object) := rfl

@[simp]
lemma SetTheory.Object.ofnat_eq'' {n:Nat} : ((n:ℕ):Object) = (n: Object) := byinst✝:SetTheoryn:Nat.toSubtype⊢ ↑(Set.nat_equiv.symm n) = ↑n
  simp [instNatCast, Nat.cast, Set.instNatCast]All goals completed! 🐙

@[simp]
lemma SetTheory.Object.ofnat_eq''' {n:ℕ} {hn} : ((⟨(n:Object), hn⟩: nat): ℕ) = n := byinst✝:SetTheoryn:ℕhn:↑n ∈ nat⊢ Set.nat_equiv.symm ⟨↑n, hn⟩ = n
  simp [instNatCast, Nat.cast, Set.instNatCast]All goals completed! 🐙

lemma SetTheory.Set.nat_coe_eq {n:ℕ} : (n:Nat) = OfNat.ofNat n := rfl

@[simp]
lemma SetTheory.Set.nat_equiv_inj (n m:ℕ) : (n:Nat) = (m:Nat) ↔ n=m  :=
  Equiv.apply_eq_iff_eq nat_equiv

@[simp]
lemma SetTheory.Set.nat_equiv_symm_inj (n m:Nat) : (n:ℕ) = (m:ℕ) ↔ n = m :=
  Equiv.apply_eq_iff_eq nat_equiv.symm

@[simp]
theorem SetTheory.Set.ofNat_inj (n m:ℕ) :
    (ofNat(n) : Nat) = (ofNat(m) : Nat) ↔ ofNat(n) = ofNat(m) := byinst✝:SetTheoryn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m
      convert nat_equiv_inj _ _All goals completed! 🐙

example : (5:Nat) ≠ (3:Nat) := byinst✝:SetTheory⊢ 5 ≠ 3
  simpAll goals completed! 🐙

@[simp]
theorem SetTheory.Set.ofNat_inj' (n m:ℕ) :
    (ofNat(n) : Object) = (ofNat(m) : Object) ↔ ofNat(n) = ofNat(m) := byinst✝:SetTheoryn:ℕm:ℕ⊢ OfNat.ofNat n = OfNat.ofNat m ↔ OfNat.ofNat n = OfNat.ofNat m
      simp only [←Object.ofnat_eq, Object.ofnat_eq', Set.coe_inj, Set.nat_equiv_inj]inst✝:SetTheoryn:ℕm:ℕ⊢ n = m ↔ OfNat.ofNat n = OfNat.ofNat m
      rflAll goals completed! 🐙

example : (5:Object) ≠ (3:Object) := byinst✝:SetTheory⊢ 5 ≠ 3
  simpAll goals completed! 🐙

@[simp]
lemma SetTheory.Set.nat_coe_eq_iff {m n : ℕ} : (m:Object) = ofNat(n) ↔ m = n := byinst✝:SetTheorym:ℕn:ℕ⊢ ↑m = OfNat.ofNat n ↔ m = n exact ofNat_inj' m nAll goals completed! 🐙

example (n: ℕ) : (n: Object) = 2 ↔ n = 2 := byinst✝:SetTheoryn:ℕ⊢ ↑n = 2 ↔ n = 2
  simpAll goals completed! 🐙

@[simp]
theorem SetTheory.Object.natCast_inj (n m:ℕ) :
    (n : Object) = (m : Object) ↔ n = m := byinst✝:SetTheoryn:ℕm:ℕ⊢ ↑n = ↑m ↔ n = m
      simp [←ofnat_eq, Subtype.val_inj]All goals completed! 🐙

@[simp]
lemma SetTheory.Set.nat_equiv_coe_of_coe (n:ℕ) : ((n:Nat):ℕ) = n :=
  Equiv.symm_apply_apply nat_equiv n

@[simp]
lemma SetTheory.Set.nat_equiv_coe_of_coe' (n:Nat) : ((n:ℕ):Nat) = n :=
  Equiv.symm_apply_apply nat_equiv.symm n

@[simp]
lemma SetTheory.Set.nat_equiv_coe_of_coe'' (n:ℕ) : ((ofNat(n):Nat):ℕ) = n :=
  nat_equiv_coe_of_coe n

@[simp]
lemma SetTheory.Set.nat_coe_eq_iff' {m: Nat} {n : ℕ} : (m:Object) = (ofNat(n):Object) ↔ (m:ℕ) = ofNat(n) := byinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ ↑m = OfNat.ofNat n ↔ nat_equiv.symm m = OfNat.ofNat n
  constructormpinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ ↑m = OfNat.ofNat n → nat_equiv.symm m = OfNat.ofNat nmprinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ nat_equiv.symm m = OfNat.ofNat n → ↑m = OfNat.ofNat n <;>mpinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ ↑m = OfNat.ofNat n → nat_equiv.symm m = OfNat.ofNat nmprinst✝:SetTheorym:Nat.toSubtypen:ℕ⊢ nat_equiv.symm m = OfNat.ofNat n → ↑m = OfNat.ofNat n intro hmprinst✝:SetTheorym:Nat.toSubtypen:ℕh:nat_equiv.symm m = OfNat.ofNat n⊢ ↑m = OfNat.ofNat n <;>mpinst✝:SetTheorym:Nat.toSubtypen:ℕh:↑m = OfNat.ofNat n⊢ nat_equiv.symm m = OfNat.ofNat nmprinst✝:SetTheorym:Nat.toSubtypen:ℕh:nat_equiv.symm m = OfNat.ofNat n⊢ ↑m = OfNat.ofNat n rw [show m = n by aesop]mprinst✝:SetTheorym:Nat.toSubtypen:ℕh:nat_equiv.symm m = OfNat.ofNat n⊢ ↑↑n = OfNat.ofNat n
  apply nat_equiv_coe_of_coemprinst✝:SetTheorym:Nat.toSubtypen:ℕh:nat_equiv.symm m = OfNat.ofNat n⊢ ↑↑n = OfNat.ofNat n; rflAll goals completed! 🐙

Приклад 3.1.16 (спрощений).

example : ({3, 5}:Set) ⊆ {1, 3, 5} := byinst✝:SetTheory⊢ {3, 5} ⊆ {1, 3, 5}
  simp only [subset_def, mem_pair, mem_triple]inst✝:SetTheory⊢ ∀ (x : Object), x = 3 ∨ x = 5 → x = 1 ∨ x = 3 ∨ x = 5; tautoAll goals completed! 🐙

Приклад 3.1.17 (спрощений).

example : ({3, 5}:Set).specify (fun x ↦ x.val ≠ 3) = ({5}:Set) := byinst✝:SetTheory⊢ ({3, 5}.specify fun x => ↑x ≠ 3) = {5}
  exthinst✝:SetTheoryx✝:Object⊢ (x✝ ∈ {3, 5}.specify fun x => ↑x ≠ 3) ↔ x✝ ∈ {5}
  simp only [mem_singleton, specification_axiom'']hinst✝:SetTheoryx✝:Object⊢ (∃ (_ : x✝ ∈ {3, 5}), x✝ ≠ 3) ↔ x✝ = 5
  constructorh.mpinst✝:SetTheoryx✝:Object⊢ (∃ (_ : x✝ ∈ {3, 5}), x✝ ≠ 3) → x✝ = 5h.mprinst✝:SetTheoryx✝:Object⊢ x✝ = 5 → ∃ (_ : x✝ ∈ {3, 5}), x✝ ≠ 3
  ·h.mpinst✝:SetTheoryx✝:Object⊢ (∃ (_ : x✝ ∈ {3, 5}), x✝ ≠ 3) → x✝ = 5 rintro ⟨h1, h2⟩h.mp.introinst✝:SetTheoryx✝:Objecth1:x✝ ∈ {3, 5}h2:x✝ ≠ 3⊢ x✝ = 5; simp only [mem_pair] at h1h.mp.introinst✝:SetTheoryx✝:Objecth2:x✝ ≠ 3h1:x✝ = 3 ∨ x✝ = 5⊢ x✝ = 5; tautoAll goals completed! 🐙
  rintro ⟨rfl⟩h.mpr.reflinst✝:SetTheory⊢ ∃ (_ : 5 ∈ {3, 5}), 5 ≠ 3; norm_numAll goals completed! 🐙

Приклад 3.1.24

example : ({1, 2, 4}:Set) ∩ {2,3,4} = {2, 4} := byinst✝:SetTheory⊢ {1, 2, 4} ∩ {2, 3, 4} = {2, 4}
  ext xhinst✝:SetTheoryx:Object⊢ x ∈ {1, 2, 4} ∩ {2, 3, 4} ↔ x ∈ {2, 4}
  -- Замість того щоб розгортати повторювані варіанти вручну, як раніше,
  -- можна використати тактику `aesop`, яка робить це автоматично.
  aesopAll goals completed! 🐙

Приклад 3.1.24

example : ({1, 2}:Set) ∩ {3,4} = ∅ := byinst✝:SetTheory⊢ {1, 2} ∩ {3, 4} = ∅
  rw [eq_empty_iff_forall_notMem]inst✝:SetTheory⊢ ∀ (x : Object), x ∉ {1, 2} ∩ {3, 4}
  aesopAll goals completed! 🐙

example : ¬ Disjoint ({1, 2, 3}:Set) {2,3,4} := byinst✝:SetTheory⊢ ¬Disjoint {1, 2, 3} {2, 3, 4}
  rw [disjoint_iff]inst✝:SetTheory⊢ ¬{1, 2, 3} ∩ {2, 3, 4} = ∅
  intro hinst✝:SetTheoryh:{1, 2, 3} ∩ {2, 3, 4} = ∅⊢ False
  change {1, 2, 3} ∩ {2, 3, 4} = ∅ at hinst✝:SetTheoryh:{1, 2, 3} ∩ {2, 3, 4} = ∅⊢ False
  rw [eq_empty_iff_forall_notMem] at hinst✝:SetTheoryh:∀ (x : Object), x ∉ {1, 2, 3} ∩ {2, 3, 4}⊢ False
  aesopAll goals completed! 🐙

declaration uses 'sorry'example : Disjoint (∅:Set) ∅ := byinst✝:SetTheory⊢ Disjoint ∅ ∅ sorryAll goals completed! 🐙

Визначення 3.1.26 приклад

example : ({1, 2, 3, 4}:Set) \ {2,4,6} = {1, 3} := byinst✝:SetTheory⊢ {1, 2, 3, 4} \ {2, 4, 6} = {1, 3}
  apply exthinst✝:SetTheory⊢ ∀ (x : Object), x ∈ {1, 2, 3, 4} \ {2, 4, 6} ↔ x ∈ {1, 3}; aesopAll goals completed! 🐙

Приклад 3.1.30

declaration uses 'sorry'example : ({3,5,9}:Set).replace (P := fun x y ↦ ∃ (n:ℕ), x.val = n ∧ y = (n+1:ℕ)) (byinst✝:SetTheory⊢ ∀ (x : {3, 5, 9}.toSubtype) (y y' : Object),
  (fun x y => ∃ n, ↑x = ↑n ∧ y = ↑(n + 1)) x y ∧ (fun x y => ∃ n, ↑x = ↑n ∧ y = ↑(n + 1)) x y' → y = y' aesopAll goals completed! 🐙)
  = {4,6,10} := byinst✝:SetTheory⊢ {3, 5, 9}.replace ⋯ = {4, 6, 10} sorryAll goals completed! 🐙

Приклад 3.1.31

example : ({3,5,9}:Set).replace (P := fun _ y ↦ y=1) (byinst✝:SetTheory⊢ ∀ (x : {3, 5, 9}.toSubtype) (y y' : Object), (fun x y => y = 1) x y ∧ (fun x y => y = 1) x y' → y = y' aesopAll goals completed! 🐙) = {1} := byinst✝:SetTheory⊢ {3, 5, 9}.replace ⋯ = {1}
  exthinst✝:SetTheoryx✝:Object⊢ x✝ ∈ {3, 5, 9}.replace ⋯ ↔ x✝ ∈ {1}; simp only [replacement_axiom]hinst✝:SetTheoryx✝:Object⊢ (∃ x, x✝ = 1) ↔ x✝ ∈ {1}; aesopAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.subset_tfae (A B:Set) : [A ⊆ B, A ∪ B = B, A ∩ B = A].TFAE := byinst✝:SetTheoryA:SetB:Set⊢ [A ⊆ B, A ∪ B = B, A ∩ B = A].TFAE sorryAll goals completed! 🐙

Вправа 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.inter_subset_left (A B:Set) : A ∩ B ⊆ A := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ B ⊆ A
  sorryAll goals completed! 🐙

Вправа 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.inter_subset_right (A B:Set) : A ∩ B ⊆ B := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ B ⊆ B
  sorryAll goals completed! 🐙

Вправа 3.1.7

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.subset_inter_iff (A B C:Set) : C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B := byinst✝:SetTheoryA:SetB:SetC:Set⊢ C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B
  sorryAll goals completed! 🐙

Вправа 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.subset_union_left (A B:Set) : A ⊆ A ∪ B := byinst✝:SetTheoryA:SetB:Set⊢ A ⊆ A ∪ B
  sorryAll goals completed! 🐙

Вправа 3.1.7

theorem declaration uses 'sorry'SetTheory.Set.subset_union_right (A B:Set) : B ⊆ A ∪ B := byinst✝:SetTheoryA:SetB:Set⊢ B ⊆ A ∪ B
  sorryAll goals completed! 🐙

Вправа 3.1.7

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.union_subset_iff (A B C:Set) : A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C := byinst✝:SetTheoryA:SetB:SetC:Set⊢ A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C
  sorryAll goals completed! 🐙

Вправа 3.1.8

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.inter_union_cancel (A B:Set) : A ∩ (A ∪ B) = A := byinst✝:SetTheoryA:SetB:Set⊢ A ∩ (A ∪ B) = A sorryAll goals completed! 🐙

Вправа 3.1.8

@[simp]
theorem declaration uses 'sorry'SetTheory.Set.union_inter_cancel (A B:Set) : A ∪ (A ∩ B) = A := byinst✝:SetTheoryA:SetB:Set⊢ A ∪ A ∩ B = A sorryAll goals completed! 🐙

Вправа 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.partition_left {A B X:Set} (h_union: A ∪ B = X) (h_inter: A ∩ B = ∅) :
    A = X \ B := byinst✝:SetTheoryA:SetB:SetX:Seth_union:A ∪ B = Xh_inter:A ∩ B = ∅⊢ A = X \ B sorryAll goals completed! 🐙

Вправа 3.1.9

theorem declaration uses 'sorry'SetTheory.Set.partition_right {A B X:Set} (h_union: A ∪ B = X) (h_inter: A ∩ B = ∅) :
    B = X \ A := byinst✝:SetTheoryA:SetB:SetX:Seth_union:A ∪ B = Xh_inter:A ∩ B = ∅⊢ B = X \ A
  sorryAll goals completed! 🐙

Вправа 3.1.10. Вам можуть стати в пригоді Function.onFun_apply.{u_1, u_2, u_3} {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : β → β → γ) (g : α → β) (a b : α) : Function.onFun f g a b = f (g a) (g b)Function.onFun_apply та тактика Unknown identifier `fin_cases`fin_cases.

theorem declaration uses 'sorry'SetTheory.Set.pairwise_disjoint (A B:Set) :
    Pairwise (Function.onFun Disjoint ![A \ B, A ∩ B, B \ A]) := byinst✝:SetTheoryA:SetB:Set⊢ Pairwise (Function.onFun Disjoint ![A \ B, A ∩ B, B \ A]) sorryAll goals completed! 🐙

Вправа 3.1.10

theorem declaration uses 'sorry'SetTheory.Set.union_eq_partition (A B:Set) : A ∪ B = (A \ B) ∪ (A ∩ B) ∪ (B \ A) := byinst✝:SetTheoryA:SetB:Set⊢ A ∪ B = A \ B ∪ A ∩ B ∪ B \ A
  sorryAll goals completed! 🐙

Вправа 3.1.11. Завдання полягає в тому, щоб довести це без використання Unknown constant `specify`Set.specify, Unknown constant `specification_axiom`Set.specification_axiom або Unknown constant `specification_axiom`Set.specification_axiom, або будь-чого, побудованого із них (наприклад, різниці та перетини)..

theorem declaration uses 'sorry'SetTheory.Set.specification_from_replacement {A:Set} {P: A → Prop} :
    ∃ B, B ⊆ A ∧ ∀ x, x.val ∈ B ↔ P x := byinst✝:SetTheoryA:SetP:A.toSubtype → Prop⊢ ∃ B ⊆ A, ∀ (x : A.toSubtype), ↑x ∈ B ↔ P x sorryAll goals completed! 🐙

Вправа 3.1.12.

theorem declaration uses 'sorry'SetTheory.Set.subset_union_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) :
    A' ∪ B' ⊆ A ∪ B := byinst✝:SetTheoryA:SetB:SetA':SetB':SethA'A:A' ⊆ AhB'B:B' ⊆ B⊢ A' ∪ B' ⊆ A ∪ B sorryAll goals completed! 🐙

Вправа 3.1.12.

theorem declaration uses 'sorry'SetTheory.Set.subset_inter_subset {A B A' B':Set} (hA'A: A' ⊆ A) (hB'B: B' ⊆ B) :
    A' ∩ B' ⊆ A ∩ B := byinst✝:SetTheoryA:SetB:SetA':SetB':SethA'A:A' ⊆ AhB'B:B' ⊆ B⊢ A' ∩ B' ⊆ A ∩ B sorryAll goals completed! 🐙

Вправа 3.1.12.

theorem declaration uses 'sorry'SetTheory.Set.subset_diff_subset_counter :
    ∃ (A B A' B':Set), (A' ⊆ A) ∧ (B' ⊆ B) ∧ ¬ (A' \ B') ⊆ (A \ B) := byinst✝:SetTheory⊢ ∃ A B A' B', A' ⊆ A ∧ B' ⊆ B ∧ ¬A' \ B' ⊆ A \ B sorryAll goals completed! 🐙

/-
  Заключна частина Вправи 3.1.12: сформулюйте та доведіть обґрунтований позитивний результат
  заміни для вищенаведеної теореми, який включає різниці множин.
-/

Вправа 3.1.13

theorem declaration uses 'sorry'SetTheory.Set.singleton_iff (A:Set) (hA: A ≠ ∅) : (¬∃ B ⊂ A, B ≠ ∅) ↔ ∃ x, A = {x} := byinst✝:SetTheoryA:SethA:A ≠ ∅⊢ (¬∃ B ⊂ A, B ≠ ∅) ↔ ∃ x, A = {x} sorryAll goals completed! 🐙

/-
  Тепер ми введемо зв'язки між цим поняттям множини та поняттям Mathlib.
  Вправа нижче ознайомить вас з API для множин Mathlib.
-/

instance SetTheory.Set.inst_coe_set : Coe Set (_root_.Set Object) where
  coe X := { x | x ∈ X }

-- Тепер ми можемо перетворити наш `Set` на `_root_.Set` з Mathlib.
-- Зауважте, що множини в Mathlib параметризуються типом елементів, у нашому випадку — `Object`.
example (X: Set) : _root_.Set Object := X

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

@[simp]
theorem SetTheory.Set.coe_inj' (X Y:Set) :
    (X : _root_.Set Object) = (Y : _root_.Set Object) ↔ X = Y := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} = {x | x ∈ Y} ↔ X = Y
  constructormpinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} = {x | x ∈ Y} → X = Ymprinst✝:SetTheoryX:SetY:Set⊢ X = Y → {x | x ∈ X} = {x | x ∈ Y}
  .mpinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} = {x | x ∈ Y} → X = Y intro hmpinst✝:SetTheoryX:SetY:Seth:{x | x ∈ X} = {x | x ∈ Y}⊢ X = Y; apply extmp.hinst✝:SetTheoryX:SetY:Seth:{x | x ∈ X} = {x | x ∈ Y}⊢ ∀ (x : Object), x ∈ X ↔ x ∈ Y; intro xmp.hinst✝:SetTheoryX:SetY:Seth:{x | x ∈ X} = {x | x ∈ Y}x:Object⊢ x ∈ X ↔ x ∈ Y
    replace h := congr(x ∈ $h)mp.hinst✝:SetTheoryX:SetY:Setx:Objecth:?_mvar.127178 := id (congrArg (fun x => _fvar.127174 ∈ x) _fvar.127156)⊢ x ∈ X ↔ x ∈ Y; simpa using hAll goals completed! 🐙
  rintro rflmprinst✝:SetTheoryX:Set⊢ {x | x ∈ X} = {x | x ∈ X}; rflAll goals completed! 🐙

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

theorem SetTheory.Set.mem_coe (X:Set) (x:Object) : x ∈ (X : _root_.Set Object) ↔ x ∈ X := byinst✝:SetTheoryX:Setx:Object⊢ x ∈ {x | x ∈ X} ↔ x ∈ X
  simpAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_empty : ((∅:Set) : _root_.Set Object) = ∅ := byinst✝:SetTheory⊢ {x | x ∈ ∅} = ∅ sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_subset (X Y:Set) :
    (X : _root_.Set Object) ⊆ (Y : _root_.Set Object) ↔ X ⊆ Y := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} ⊆ {x | x ∈ Y} ↔ X ⊆ Y sorryAll goals completed! 🐙

theorem declaration uses 'sorry'SetTheory.Set.coe_ssubset (X Y:Set) :
    (X : _root_.Set Object) ⊂ (Y : _root_.Set Object) ↔ X ⊂ Y := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X} ⊂ {x | x ∈ Y} ↔ X ⊂ Y sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_singleton (x: Object) : (({x}:Set) : _root_.Set Object) = {x} := byinst✝:SetTheoryx:Object⊢ {x_1 | x_1 ∈ {x}} = {x} sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_union (X Y: Set) :
    ((X ∪ Y:Set) : _root_.Set Object) = (X : _root_.Set Object) ∪ (Y : _root_.Set Object) := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X ∪ Y} = {x | x ∈ X} ∪ {x | x ∈ Y} sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_pair (x y: Object) : (({x, y}:Set) : _root_.Set Object) = {x, y} := byinst✝:SetTheoryx:Objecty:Object⊢ {x_1 | x_1 ∈ {x, y}} = {x, y} sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_subtype (X: Set) :  (X : _root_.Set Object) = X.toSubtype := byinst✝:SetTheoryX:Set⊢ ↑{x | x ∈ X} = X.toSubtype sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_intersection (X Y: Set) :
    ((X ∩ Y:Set) : _root_.Set Object) = (X : _root_.Set Object) ∩ (Y : _root_.Set Object) := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X ∩ Y} = {x | x ∈ X} ∩ {x | x ∈ Y} sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_diff (X Y: Set) :
    ((X \ Y:Set) : _root_.Set Object) = (X : _root_.Set Object) \ (Y : _root_.Set Object) := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ X \ Y} = {x | x ∈ X} \ {x | x ∈ Y} sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_Disjoint (X Y: Set) :
    Disjoint (X : _root_.Set Object) (Y : _root_.Set Object) ↔ Disjoint X Y := byinst✝:SetTheoryX:SetY:Set⊢ Disjoint {x | x ∈ X} {x | x ∈ Y} ↔ Disjoint X Y sorryAll goals completed! 🐙

end Chapter3