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

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

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

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

Тип множин Chapter3.SetTheory.Set [self : Chapter3.SetTheory] : TypeChapter3.SetTheory.Set
Тип об'єктів Chapter3.SetTheory.Object [self : Chapter3.SetTheory] : TypeChapter3.SetTheory.Object
Аксіома що кожна множина є (або може бути перетворена на) об'єкт
Порожня множина ∅ : ?m.54421∅, сінглетони 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.54191X ∪ 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.54334) (y y' : ?m.54349 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 [self : Chapter3.SetTheory] : TypeChapter3.Set, визначеним тут, хоча ми спробуємо зробити позначення максимально збігаючимися. Це спричиняє певний конфлікт позначень: наприклад, може знадобитися явно вказати (∅:failed to synthesize Chapter3.SetTheory Additional diagnostic information may be available using the `set_option diagnostics true` command.Chapter3.Set) замість просто ∅ : ?m.54421∅, щоб вказати, що використовується версія порожньої множини Chapter3.SetTheory.Set [self : Chapter3.SetTheory] : TypeChapter3.Set, а не версія порожньої множини Mathlib, і аналогічно для інших позначень, визначених тут.
В Аналізі I ми вирішили працювати з "нечистою" теорією множин, в якій може бути більше unknown identifier 'Object'Object-ів, ніж просто Set.{u} (α : Type u) : Type uSet-ів. У теорії типів Lean це вимагає розглядати Chapter3.SetTheory.Set [self : Chapter3.SetTheory] : TypeChapter3.Set та Chapter3.SetTheory.Object [self : Chapter3.SetTheory] : TypeChapter3.Object як окремі типи. Іноді це означає, що нам доводиться використовувати приведення unknown identifier 'X.toObject'X.toObject від Chapter3.SetTheory.Set [self : Chapter3.SetTheory] : TypeChapter3.Set unknown identifier 'X'X, щоб перетворити його на Chapter3.SetTheory.Object [self : Chapter3.SetTheory] : TypeChapter3.Object: це здебільшого потрібно під час маніпулювання множинами множин.
Після завершення цього розділу поняття Chapter3.SetTheory.Set [self : Chapter3.SetTheory] : TypeChapter3.SetTheory.Set буде відхилено на користь стандартного позначення Set.{u} (α : Type u) : Type uSet від Mathlib (або, точніше, типу Set sorry : Type u_1Set unknown identifier 'X'X множини в заданому типі unknown identifier 'X'X). Однак, через різні технічні несумісності між теорією множин та теорією типів, ми не намагатимемося створити будь-яку еквівалентність між цими двома поняттями множин. (Таким чином, це робить весь цей розділ необов'язковим з точки зору решти книги, хоча ми зберігаємо його для педагогічних цілей.)

namespace Chapter3

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

class SetTheory where
  Set : Type -- Аксіома 3.1
  Object : Type -- Аксіома 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
  power_set_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

export SetTheory (Set Object)

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

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

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

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

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

abbrev SetTheory.Set.toObject (X:Set) : Object := X

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

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

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

@[simp]
theorem SetTheory.Set.coe_eq_iff (X Y:Set) : X.toObject = Y.toObject ↔  X = Y := byinst✝:SetTheoryX:SetY:Set⊢ X.toObject = Y.toObject ↔ X = Y
  constructormpinst✝:SetTheoryX:SetY:Set⊢ X.toObject = Y.toObject → X = Ymprinst✝:SetTheoryX:SetY:Set⊢ X = Y → X.toObject = Y.toObject
  .mpinst✝:SetTheoryX:SetY:Set⊢ X.toObject = Y.toObject → X = Y exact coe_eqAll goals completed! 🐙
  intro hmprinst✝:SetTheoryX:SetY:Seth:X = Y⊢ X.toObject = Y.toObject; subst hmprinst✝:SetTheoryX:Set⊢ X.toObject = X.toObject; rflAll goals completed! 🐙

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

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

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

theorem SetTheory.Set.ext_iff (X Y: Set) : X = Y ↔ ∀ x, x ∈ X ↔ x ∈ Y := byinst✝:SetTheoryX:SetY:Set⊢ X = Y ↔ ∀ (x : Object), x ∈ X ↔ x ∈ Y
  constructormpinst✝:SetTheoryX:SetY:Set⊢ X = Y → ∀ (x : Object), x ∈ X ↔ x ∈ Ymprinst✝:SetTheoryX:SetY:Set⊢ (∀ (x : Object), x ∈ X ↔ x ∈ Y) → X = Y
  .mpinst✝:SetTheoryX:SetY:Set⊢ X = Y → ∀ (x : Object), x ∈ X ↔ x ∈ Y intro hmpinst✝:SetTheoryX:SetY:Seth:X = Y⊢ ∀ (x : Object), x ∈ X ↔ x ∈ Y; subst hmpinst✝:SetTheoryX:Set⊢ ∀ (x : Object), x ∈ X ↔ x ∈ X; simpAll goals completed! 🐙
  .mprinst✝:SetTheoryX:SetY:Set⊢ (∀ (x : Object), x ∈ X ↔ x ∈ Y) → X = Y intro hmprinst✝:SetTheoryX:SetY:Seth:∀ (x : Object), x ∈ X ↔ x ∈ Y⊢ X = Y; apply extmpr.hinst✝:SetTheoryX:SetY:Seth:∀ (x : Object), x ∈ X ↔ x ∈ Y⊢ ∀ (x : Object), x ∈ X ↔ x ∈ Y; exact hAll goals completed! 🐙

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

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

@[simp]
theorem SetTheory.Set.not_mem_empty : ∀ x, x ∉ (∅:Set) := SetTheory.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! 🐙
  replace claim := ext 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 := SetTheory.singleton

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

@[simp]
theorem SetTheory.Set.mem_singleton (x a:Object) : x ∈ ({a}:Set) ↔ x = a := byinst✝:SetTheoryx:Objecta:Object⊢ x ∈ {a} ↔ x = a
  exact SetTheory.singleton_axiom x aAll goals completed! 🐙

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

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

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

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

Аксіома 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:Object) : x ∈ ({a,b,c}:Set) ↔ (x = a ∨ x = b ∨ x = c) := byinst✝:SetTheoryc:Objectx:Objecta:Objectb:Object⊢ x ∈ {a, b, c} ↔ x = a ∨ x = b ∨ x = c
  simp [Insert.insert, mem_union, mem_singleton]All goals completed! 🐙

Ремарка 3.1.8

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

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

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

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.toObject}abbrev SetTheory.Set.pair_empty : Set := {empty.toObject, singleton_empty.toObject}

Вправа 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)
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  apply exthinst✝:SetTheoryA:SetB:SetC:Set⊢ ∀ (x : Object), x ∈ A ∪ B ∪ C ↔ x ∈ A ∪ (B ∪ C)
  intro 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)
    rcases hx with case1 | case2h.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)
      rcases case1 with case1a | case1bh.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:x ∈ B ∪ C⊢ 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:x ∈ B ∪ C⊢ x ∈ A ∨ x ∈ B ∪ C; tautoAll goals completed! 🐙
  sorryAll goals completed! 🐙

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

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)

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

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

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 declaration uses 'sorry'SetTheory.Set.pair_union_pair (a b c:Object) :
    ({a,b}:Set) ∪ {b,c} = {a,b,c} := sorry

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

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

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

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

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

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

Приклади 3.1.16

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
  replace hx := hAB x hxinst✝:SetTheoryA:SetB:SetC:SethAB:∀ x ∈ A, x ∈ BhBC:B ⊆ Cx:Objecthx:x ∈ B⊢ x ∈ C
  replace hx := hBC x 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! 🐙

This defines the subtype unknown identifier 'A.toSubtype'A.toSubtype for any . To produce an element unknown identifier 'x''x' of this subtype, use invalid constructor ⟨...⟩, expected type must be an inductive type ?m.54738⟨ x, hx ⟩, where and . The object unknown identifier 'x'x associated to a subtype element unknown identifier 'x''x' is recovered as unknown identifier 'x.val'x.val, and the property unknown identifier 'hx'hx that unknown identifier 'x'x belongs to unknown identifier 'A'A is recovered as unknown identifier 'x.property'x.property Це визначає підтип unknown identifier 'A.toSubtype'A.toSubtype для будь-якого . Щоб створити елемент unknown identifier 'x''x' цього підтипу, використовуйте invalid constructor ⟨...⟩, expected type must be an inductive type ?m.54738⟨ 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)

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

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

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 ⟩

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.toSubtype) :
    x.val ∈ A.specify P ↔ P x :=
  (SetTheory.specification_axiom A P).2 x

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

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⟩
    have h' := specification_axiom hmpinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ A.specify Ph':x ∈ A⊢ ∃ (h : x ∈ A), P ⟨x, h⟩
    use h'hinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ A.specify Ph':x ∈ A⊢ P ⟨x, h'⟩
    rw [←specification_axiom' P ⟨ x, h' ⟩ ]hinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ A.specify Ph':x ∈ A⊢ ↑⟨x, h'⟩ ∈ A.specify P
    simp [h]All goals completed! 🐙
  intro hmprinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:∃ (h : x ∈ A), P ⟨x, h⟩⊢ x ∈ A.specify P
  obtain ⟨ h, hP ⟩ := hmpr.introinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ AhP:P ⟨x, h⟩⊢ x ∈ A.specify P
  rw [←specification_axiom' P ⟨ x,h ⟩ ] at hPmpr.introinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ AhP:↑⟨x, h⟩ ∈ A.specify P⊢ x ∈ A.specify P
  simp at hPmpr.introinst✝:SetTheoryA:SetP:A.toSubtype → Propx:Objecth:x ∈ AhP:x ∈ A.specify P⊢ x ∈ A.specify P; assumptionAll 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)

Визначення 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':x ∈ X⊢ x ∈ X ∧ x ∈ Y
    simp [h']mpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X ∩ Yh':x ∈ X⊢ 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)

Визначення 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':x ∈ X⊢ x ∈ X ∧ x ∉ Y
    simp [h']mpinst✝:SetTheoryx:ObjectX:SetY:Seth:x ∈ X \ Yh':x ∈ X⊢ 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)

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) := sorry

Твердження 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) := sorry

Твердження 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} (hAX: A ⊆ X) : A ∩ (X \ A) = ∅ := byinst✝:SetTheoryA:SetX:SethAX:A ⊆ X⊢ A ∩ (X \ A) = ∅ sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.compl_union {A B X:Set} (hAX: A ⊆ X) (hBX: B ⊆ X) :
    X \ (A ∪ B) = (X \ A) ∩ (X \ B) := byinst✝:SetTheoryA:SetB:SetX:SethAX:A ⊆ XhBX:B ⊆ X⊢ 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} (hAX: A ⊆ X) (hBX: B ⊆ X) :
    X \ (A ∩ B) = (X \ A) ∪ (X \ B) := byinst✝:SetTheoryA:SetB:SetX:SethAX:A ⊆ XhBX:B ⊆ X⊢ 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]inst✝:SetTheoryX:SetY:SetZ:Set⊢ X ∪ Y ∩ Z ⊆ X ∪ Y ∩ Z
    exact subset_self _All goals completed! 🐙

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

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

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

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 (Аксіомна схема підстановки)

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

Аксіома 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

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

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

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

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

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

lemma SetTheory.Object.ofnat_eq' {n:ℕ} : (ofNat(n):Object) = (n:Object) := rfllemma 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! 🐙

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

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

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

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

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

declaration uses 'sorry'example : ({3, 5}:Set) ⊆ {1, 3, 5} := byinst✝:SetTheory⊢ {3, 5} ⊆ {1, 3, 5}
  sorryAll goals completed! 🐙

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

declaration uses 'sorry'example : ({3, 5}:Set).specify (fun x ↦ x.val ≠ 3)
 = {(5:Object)} := byinst✝:SetTheory⊢ ({3, 5}.specify fun x => ↑x ≠ 3) = {5}
  sorryAll goals completed! 🐙

Приклад 3.1.24

declaration uses 'sorry'example : ({1, 2, 4}:Set) ∩ {2,3,4} = {2, 4} := byinst✝:SetTheory⊢ {1, 2, 4} ∩ {2, 3, 4} = {2, 4} sorryAll goals completed! 🐙

Приклад 3.1.24

declaration uses 'sorry'example : ({1, 2}:Set) ∩ {3,4} = ∅ := byinst✝:SetTheory⊢ {1, 2} ∩ {3, 4} = ∅ sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ Disjoint  ({1, 2, 3}:Set)  {2,3,4} := byinst✝:SetTheory⊢ ¬Disjoint {1, 2, 3} {2, 3, 4} sorryAll goals completed! 🐙

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

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

declaration uses 'sorry'example : ({1, 2, 3, 4}:Set) \ {2,4,6} = {1, 3} := byinst✝:SetTheory⊢ {1, 2, 3, 4} \ {2, 4, 6} = {1, 3} sorryAll 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' sorryAll goals completed! 🐙) = {4,6,10} := byinst✝:SetTheory⊢ {3, 5, 9}.replace ⋯ = {4, 6, 10} sorryAll goals completed! 🐙

Приклад 3.1.31

declaration uses 'sorry'example : ({3,5,9}:Set).replace (P := fun x 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' sorryAll goals completed! 🐙) = {1} := byinst✝:SetTheory⊢ {3, 5, 9}.replace ⋯ = {1} sorryAll 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 C:Set) : [A ⊆ B, A ∪ B = B, A ∩ B = A].TFAE := byinst✝:SetTheoryA:SetB:SetC: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

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

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

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

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

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 'Set.specify'Set.specify, unknown constant 'Set.specification_axiom'Set.specification_axiom або unknown constant 'Set.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 }

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

@[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
    apply_fun (fun S ↦ x ∈ S) at hmp.hinst✝:SetTheoryX:SetY:Setx:Objecth:(x ∈ {x | x ∈ X}) = (x ∈ {x | x ∈ Y})⊢ x ∈ X ↔ x ∈ Y
    simp at hmp.hinst✝:SetTheoryX:SetY:Setx:Objecth:x ∈ X ↔ x ∈ Y⊢ x ∈ X ↔ x ∈ Y; assumptionAll goals completed! 🐙
  intro hmprinst✝:SetTheoryX:SetY:Seth:X = Y⊢ {x | x ∈ X} = {x | x ∈ Y}; subst hmprinst✝: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
  simp [Coe.coe]All 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} : _root_.Set Object) = {x} := byinst✝:SetTheoryx:Object⊢ {x} = {x} sorryAll goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.coe_union (X Y: Set) :
    (X ∪ Y : _root_.Set Object) = (X : _root_.Set Object) ∪ (Y : _root_.Set Object) := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ 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} : _root_.Set Object) = {x, y} := byinst✝:SetTheoryx:Objecty:Object⊢ {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 : _root_.Set Object) = (X : _root_.Set Object) ∩ (Y : _root_.Set Object) := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ 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 : _root_.Set Object) = (X : _root_.Set Object) \ (Y : _root_.Set Object) := byinst✝:SetTheoryX:SetY:Set⊢ {x | x ∈ 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