Аналіз I, Розділ 3.5: Декартови добутки

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

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

• Впорядковані пари та кортежі.
• Декартові добутки та n-кратні добутки.
• Зліченний вибіру.
• Зв'язок із Mathlib аналогами такими як Set.pi та Set.prod.

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

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

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

structure Chapter3.OrderedPair [SetTheory] : Type u_2

Визначення 3.5.1 (Впорядкована пара). Тут також можна було використати Object × Object для визначення OrderedPair.

• fst : Object
• snd : Object

theorem Chapter3.OrderedPair.ext_iff {inst✝ : SetTheory} {x y : OrderedPair} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

theorem Chapter3.OrderedPair.ext {inst✝ : SetTheory} {x y : OrderedPair} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y

@[simp]

theorem Chapter3.OrderedPair.eq [SetTheory] (x y x' y' : Object) : { fst := x, snd := y } = { fst := x', snd := y' } ↔ x = x' ∧ y = y'

Визначення 3.5.1 (Впорядкована пара)

theorem Chapter3.SetTheory.Set.pair_eq_singleton_iff [SetTheory] {a b c : Object} : {a, b} = {c} ↔ a = c ∧ b = c

Вспоміжна лема для Вправи 3.5.1

def Chapter3.OrderedPair.toObject [SetTheory] : OrderedPair ↪ Object

Вправа 3.5.1, перша частина

Equations

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

instance Chapter3.OrderedPair.inst_coeObject [SetTheory] : Coe OrderedPair Object

Equations

• Chapter3.OrderedPair.inst_coeObject = { coe := ⇑Chapter3.OrderedPair.toObject }

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.slice [SetTheory] (x : Object) (Y : Set) : Set

Технічна операція перетворююча об'єкт x та множину Y на множину {x} × Y, необхідна для визначення повного декартового добутку

Equations

• Chapter3.SetTheory.Set.slice x Y = Y.replace ⋯

@[simp]

theorem Chapter3.SetTheory.Set.mem_slice [SetTheory] (x z : Object) (Y : Set) : z ∈ slice x Y ↔ ∃ (y : Y.toSubtype), z = OrderedPair.toObject { fst := x, snd := ↑y }

@[reducible, inline]

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

Визначення 3.5.4 (Декартовий добуток)

Equations

• X.cartesian Y = Chapter3.SetTheory.union (X.replace ⋯)

instance Chapter3.SetTheory.Set.inst_SProd [SetTheory] : SProd Set Set Set

Цей екземпляр дозволяє використовувати позначення ×ˢ для декартового добутку.

Equations

• Chapter3.SetTheory.Set.inst_SProd = { sprod := Chapter3.SetTheory.Set.cartesian }

@[simp]

theorem Chapter3.SetTheory.Set.mem_cartesian [SetTheory] (z : Object) (X Y : Set) : z ∈ X ×ˢ Y ↔ ∃ (x : X.toSubtype) (y : Y.toSubtype), z = OrderedPair.toObject { fst := ↑x, snd := ↑y }

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.fst [SetTheory] {X Y : Set} (z : (X ×ˢ Y).toSubtype) : X.toSubtype

Equations

• Chapter3.SetTheory.Set.fst z = ⋯.choose

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.snd [SetTheory] {X Y : Set} (z : (X ×ˢ Y).toSubtype) : Y.toSubtype

Equations

• Chapter3.SetTheory.Set.snd z = ⋯.choose

theorem Chapter3.SetTheory.Set.pair_eq_fst_snd [SetTheory] {X Y : Set} (z : (X ×ˢ Y).toSubtype) : ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }

def Chapter3.SetTheory.Set.mk_cartesian [SetTheory] {X Y : Set} (x : X.toSubtype) (y : Y.toSubtype) : (X ×ˢ Y).toSubtype

Це надає OrderedPair докази того, що x ∈ X та y ∈ Y.

Equations

• Chapter3.SetTheory.Set.mk_cartesian x y = ⟨Chapter3.OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩

@[simp]

theorem Chapter3.SetTheory.Set.fst_of_mk_cartesian [SetTheory] {X Y : Set} (x : X.toSubtype) (y : Y.toSubtype) : fst (mk_cartesian x y) = x

@[simp]

theorem Chapter3.SetTheory.Set.snd_of_mk_cartesian [SetTheory] {X Y : Set} (x : X.toSubtype) (y : Y.toSubtype) : snd (mk_cartesian x y) = y

@[simp]

theorem Chapter3.SetTheory.Set.mk_cartesian_fst_snd_eq [SetTheory] {X Y : Set} (z : (X ×ˢ Y).toSubtype) : mk_cartesian (fst z) (snd z) = z

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.prod_equiv_prod [SetTheory] (X Y : Set) : ↑{x : Object | x ∈ X ×ˢ Y} ≃ ↑({x : Object | x ∈ X} ×ˢ {x : Object | x ∈ Y})

Зв’язки з добутком множин у Mathlib, який складається з пар Lean на кшталт (x, y), озброєних доказом того, що x належить лівій множині, а y — правій. Пари Lean на кшталт (x, y) подібні до нашого OrderedPair, але більш загальні.

Equations

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

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.prod_commutator [SetTheory] (X Y : Set) : (X ×ˢ Y).toSubtype ≃ (Y ×ˢ X).toSubtype

Приклад 3.5.5 / Вправа 3.6.5. Існує бієкція між X ×ˢ Y та Y ×ˢ X.

Equations

• X.prod_commutator Y = { toFun := sorry, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.curry_equiv [SetTheory] {X Y Z : Set} : (X.toSubtype → Y.toSubtype → Z.toSubtype) ≃ ((X ×ˢ Y).toSubtype → Z.toSubtype)

Приклад 3.5.5. Функцію двох змінних можна розглядати як функцію від пари.

Equations

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

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.tuple [SetTheory] {I : Set} {X : I.toSubtype → Set} (x : (i : I.toSubtype) → (X i).toSubtype) : Object

Визначення 3.5.6. Індексуюча множина I відіграє роль { i : 1 ≤ i ≤ n } у тексті. Див. Вправу 3.5.10 нижче для деяких зв’язків між цим поняттям і попереднім поняттям декартового добутку та впорядкованої пари.

Equations

• Chapter3.SetTheory.Set.tuple x = ↑fun (i : I.toSubtype) => ⟨↑(x i), ⋯⟩

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.iProd [SetTheory] {I : Set} (X : I.toSubtype → Set) : Set

Визначення 3.5.6

Equations

• Chapter3.SetTheory.Set.iProd X = (I.iUnion X ^ I).specify fun (t : (I.iUnion X ^ I).toSubtype) => ∃ (x : (i : I.toSubtype) → (X i).toSubtype), ↑t = Chapter3.SetTheory.Set.tuple x

theorem Chapter3.SetTheory.Set.mem_iProd [SetTheory] {I : Set} {X : I.toSubtype → Set} (t : Object) : t ∈ iProd X ↔ ∃ (x : (i : I.toSubtype) → (X i).toSubtype), t = tuple x

Визначення 3.5.6

theorem Chapter3.SetTheory.Set.tuple_mem_iProd [SetTheory] {I : Set} {X : I.toSubtype → Set} (x : (i : I.toSubtype) → (X i).toSubtype) : tuple x ∈ iProd X

@[simp]

theorem Chapter3.SetTheory.Set.tuple_inj [SetTheory] {I : Set} {X : I.toSubtype → Set} (x y : (i : I.toSubtype) → (X i).toSubtype) : tuple x = tuple y ↔ x = y

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.prod_associator [SetTheory] (X Y Z : Set) : ((X ×ˢ Y) ×ˢ Z).toSubtype ≃ (X ×ˢ Y ×ˢ Z).toSubtype

Приклад 3.5.8. Існує бієкція між (X ×ˢ Y) ×ˢ Z та X ×ˢ (Y ×ˢ Z).

Equations

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

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.singleton_iProd_equiv [SetTheory] (i : Object) (X : Set) : (iProd fun (x : {i}.toSubtype) => X).toSubtype ≃ X.toSubtype

Вправа 3.5.10. Я підозрюю, що більшість еквівалентностей вимагатиме класичного міркування і будуть визначені неконструктивно, але буду радий дізнатися про контрприклади.

Equations

• Chapter3.SetTheory.Set.singleton_iProd_equiv i X = { toFun := sorry, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.empty_iProd_equiv [SetTheory] (X : ∅.toSubtype → Set) : (iProd X).toSubtype ≃ Unit

Приклад 3.5.10

Equations

• Chapter3.SetTheory.Set.empty_iProd_equiv X = { toFun := sorry, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_of_const_equiv [SetTheory] (I X : Set) : (iProd fun (x : I.toSubtype) => X).toSubtype ≃ (I.toSubtype → X.toSubtype)

Приклад 3.5.10

Equations

• I.iProd_of_const_equiv X = { toFun := sorry, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_equiv_prod [SetTheory] (X : {0, 1}.toSubtype → Set) : (iProd X).toSubtype ≃ (X ⟨0, ⋯⟩ ×ˢ X ⟨1, ⋯⟩).toSubtype

Приклад 3.5.10

Equations

• Chapter3.SetTheory.Set.iProd_equiv_prod X = { toFun := sorry, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_equiv_prod_triple [SetTheory] (X : {0, 1, 2}.toSubtype → Set) : (iProd X).toSubtype ≃ (X ⟨0, ⋯⟩ ×ˢ X ⟨1, ⋯⟩ ×ˢ X ⟨2, ⋯⟩).toSubtype

Приклад 3.5.10

Equations

• Chapter3.SetTheory.Set.iProd_equiv_prod_triple X = { toFun := sorry, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_equiv_pi [SetTheory] (I : Set) (X : I.toSubtype → Set) : (iProd X).toSubtype ≃ ↑(Set.univ.pi fun (i : I.toSubtype) => {x : Object | x ∈ X i})

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

Equations

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

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.Fin [SetTheory] (n : ℕ) : Set

Тут ми створюємо аналог Mathlib-івських типів Fin n в рамках теорії множин з Розділу 3, із рудиментарним API.

Equations

• Chapter3.SetTheory.Set.Fin n = Chapter3.nat.specify fun (m : Chapter3.nat.toSubtype) => Chapter3.SetTheory.Set.nat_equiv.symm m < n

theorem Chapter3.SetTheory.Set.mem_Fin [SetTheory] (n : ℕ) (x : Object) : x ∈ Fin n ↔ ∃ m < n, x = ↑m

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.Fin_mk [SetTheory] (n m : ℕ) (h : m < n) : (Fin n).toSubtype

Equations

• Chapter3.SetTheory.Set.Fin_mk n m h = ⟨↑m, ⋯⟩

theorem Chapter3.SetTheory.Set.mem_Fin' [SetTheory] {n : ℕ} (x : (Fin n).toSubtype) : ∃ (m : ℕ) (h : m < n), x = Fin_mk n m h

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.Fin.toNat [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) : ℕ

Equations

• ↑i = ⋯.choose

noncomputable instance Chapter3.SetTheory.Set.Fin.inst_coeNat [SetTheory] {n : ℕ} : CoeOut (Fin n).toSubtype ℕ

Equations

• Chapter3.SetTheory.Set.Fin.inst_coeNat = { coe := Chapter3.SetTheory.Set.Fin.toNat }

theorem Chapter3.SetTheory.Set.Fin.toNat_spec [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) : ∃ (h : ↑i < n), i = Fin_mk n (↑i) h

theorem Chapter3.SetTheory.Set.Fin.toNat_lt [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) : ↑i < n

@[simp]

theorem Chapter3.SetTheory.Set.Fin.coe_toNat [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) : ↑↑i = ↑i

@[simp]

theorem Chapter3.SetTheory.Set.Fin.coe_inj [SetTheory] {n : ℕ} {i j : (Fin n).toSubtype} : i = j ↔ ↑i = ↑j

@[simp]

theorem Chapter3.SetTheory.Set.Fin.coe_eq_iff [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) {j : ℕ} : ↑i = ↑j ↔ ↑i = j

@[simp]

theorem Chapter3.SetTheory.Set.Fin.coe_eq_iff' [SetTheory] {n m : ℕ} (i : (Fin n).toSubtype) (hi : ↑i ∈ Fin m) : ↑⟨↑i, hi⟩ = ↑i

@[simp]

theorem Chapter3.SetTheory.Set.Fin.toNat_mk [SetTheory] {n : ℕ} (m : ℕ) (h : m < n) : ↑(Fin_mk n m h) = m

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.Fin_embed [SetTheory] (n N : ℕ) (h : n ≤ N) (i : (Fin n).toSubtype) : (Fin N).toSubtype

Equations

• Chapter3.SetTheory.Set.Fin_embed n N h i = ⟨↑i, ⋯⟩

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.Fin.Fin_equiv_Fin [SetTheory] (n : ℕ) : (Fin n).toSubtype ≃ _root_.Fin n

Зв'язки із Mathlib-овським Fin n

Equations

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

theorem Chapter3.SetTheory.Set.finite_choice [SetTheory] {n : ℕ} {X : (Fin n).toSubtype → Set} (h : ∀ (i : (Fin n).toSubtype), X i ≠ ∅) : iProd X ≠ ∅

Лема 3.5.11 (зліченний вибір)

@[reducible, inline]

abbrev Chapter3.OrderedPair.toObject' [SetTheory] : OrderedPair ↪ Object

Вправа 3.5.1, друга частина (вимагає аксіоми регулярності)

Equations

• Chapter3.OrderedPair.toObject' = { toFun := fun (p : Chapter3.OrderedPair) => Chapter3.SetTheory.set_to_object {p.fst, Chapter3.SetTheory.set_to_object {p.fst, p.snd}}, inj' := ⋯ }

structure Chapter3.SetTheory.Set.Tuple [SetTheory] (n : ℕ) : Type (max u_1 u_2)

Альтернативне визначення кортежу, використане у Вправі 3.5.2

• X : Set
• x : (Fin n).toSubtype → self.X.toSubtype
• surj : Function.Surjective self.x

theorem Chapter3.SetTheory.Set.Tuple.ext [SetTheory] {n : ℕ} {t t' : Tuple n} (hX : t.X = t'.X) (hx : ∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1)) : t = t'

Користувацька лема екстенсіональності для Вправи 3.5.2. Додавання @[ext] до структури створило б лему, що вимагала б доведення t.x = t'.x, але ці функції мають різні типи, коли t.X ≠ t'.X. Ця лема обробляє цю частину.

theorem Chapter3.SetTheory.Set.Tuple.ext_iff [SetTheory] {n : ℕ} {t t' : Tuple n} : t = t' ↔ t.X = t'.X ∧ ∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1)

theorem Chapter3.SetTheory.Set.Tuple.eq [SetTheory] {n : ℕ} (t t' : Tuple n) : t = t' ↔ ∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1)

Вправа 3.5.2

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_equiv_tuples [SetTheory] (n : ℕ) (X : (Fin n).toSubtype → Set) : (iProd X).toSubtype ≃ { t : Tuple n // ∀ (i : (Fin n).toSubtype), ↑(t.x i) ∈ X i }

Equations

• Chapter3.SetTheory.Set.iProd_equiv_tuples n X = { toFun := sorry, invFun := sorry, left_inv := ⋯, right_inv := ⋯ }

theorem Chapter3.OrderedPair.refl [SetTheory] (p : OrderedPair) : p = p

Вправа 3.5.3. Дух завдання полягає в тому, щоб уникнути прямих переписувань (які роблять усі ці твердження тривіальними), а натомість використовувати OrderedPair.eq або SetTheory.Set.tuple_inj

theorem Chapter3.OrderedPair.symm [SetTheory] (p q : OrderedPair) : p = q ↔ q = p

theorem Chapter3.OrderedPair.trans [SetTheory] {p q r : OrderedPair} (hpq : p = q) (hqr : q = r) : p = r

theorem Chapter3.SetTheory.Set.tuple_refl [SetTheory] {I : Set} {X : I.toSubtype → Set} (a : (i : I.toSubtype) → (X i).toSubtype) : tuple a = tuple a

theorem Chapter3.SetTheory.Set.tuple_symm [SetTheory] {I : Set} {X : I.toSubtype → Set} (a b : (i : I.toSubtype) → (X i).toSubtype) : tuple a = tuple b ↔ tuple b = tuple a

theorem Chapter3.SetTheory.Set.tuple_trans [SetTheory] {I : Set} {X : I.toSubtype → Set} {a b c : (i : I.toSubtype) → (X i).toSubtype} (hab : tuple a = tuple b) (hbc : tuple b = tuple c) : tuple a = tuple c

theorem Chapter3.SetTheory.Set.prod_union [SetTheory] (A B C : Set) : A ×ˢ (B ∪ C) = A ×ˢ B ∪ A ×ˢ C

Вправа 3.5.4

theorem Chapter3.SetTheory.Set.prod_inter [SetTheory] (A B C : Set) : A ×ˢ (B ∩ C) = A ×ˢ B ∩ A ×ˢ C

Вправа 3.5.4

theorem Chapter3.SetTheory.Set.prod_diff [SetTheory] (A B C : Set) : A ×ˢ (B \ C) = A ×ˢ B \ A ×ˢ C

Вправа 3.5.4

theorem Chapter3.SetTheory.Set.union_prod [SetTheory] (A B C : Set) : (A ∪ B) ×ˢ C = A ×ˢ C ∪ B ×ˢ C

Вправа 3.5.4

theorem Chapter3.SetTheory.Set.inter_prod [SetTheory] (A B C : Set) : (A ∩ B) ×ˢ C = A ×ˢ C ∩ B ×ˢ C

Вправа 3.5.4

theorem Chapter3.SetTheory.Set.diff_prod [SetTheory] (A B C : Set) : (A \ B) ×ˢ C = A ×ˢ C \ A ×ˢ B

Вправа 3.5.4

theorem Chapter3.SetTheory.Set.inter_of_prod [SetTheory] (A B C D : Set) : A ×ˢ B ∩ C ×ˢ D = (A ∩ C) ×ˢ (B ∩ D)

Вправа 3.5.5

def Chapter3.SetTheory.Set.union_of_prod [SetTheory] : Decidable (∀ (A B C D : Set), A ×ˢ B ∪ C ×ˢ D = (A ∪ C) ×ˢ (B ∪ D))

Equations

• Chapter3.SetTheory.Set.union_of_prod = sorry

def Chapter3.SetTheory.Set.diff_of_prod [SetTheory] : Decidable (∀ (A B C D : Set), A ×ˢ B \ C ×ˢ D = (A \ C) ×ˢ (B \ D))

Equations

• Chapter3.SetTheory.Set.diff_of_prod = sorry

theorem Chapter3.SetTheory.Set.prod_subset_prod [SetTheory] {A B C D : Set} (hA : A ≠ ∅) (hB : B ≠ ∅) (hC : C ≠ ∅) (hD : D ≠ ∅) : A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D

Вправа 3.5.6.

def Chapter3.SetTheory.Set.prod_subset_prod' [SetTheory] : Decidable (∀ (A B C D : Set), A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D)

Equations

• Chapter3.SetTheory.Set.prod_subset_prod' = sorry

theorem Chapter3.SetTheory.Set.direct_sum [SetTheory] {X Y Z : Set} (f : Z.toSubtype → X.toSubtype) (g : Z.toSubtype → Y.toSubtype) : ∃! h : Z.toSubtype → (X ×ˢ Y).toSubtype, fst ∘ h = f ∧ snd ∘ h = g

Вправа 3.5.7

@[simp]

theorem Chapter3.SetTheory.Set.iProd_empty_iff [SetTheory] {n : ℕ} {X : (Fin n).toSubtype → Set} : iProd X = ∅ ↔ ∃ (i : (Fin n).toSubtype), X i = ∅

Вправа 3.5.8

theorem Chapter3.SetTheory.Set.iUnion_inter_iUnion [SetTheory] {I J : Set} (A : I.toSubtype → Set) (B : J.toSubtype → Set) : I.iUnion A ∩ J.iUnion B = (I ×ˢ J).iUnion fun (p : (I ×ˢ J).toSubtype) => A (fst p) ∩ B (snd p)

Вправа 3.5.9

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.graph [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) : Set

Equations

• Chapter3.SetTheory.Set.graph f = (X ×ˢ Y).specify fun (p : (X ×ˢ Y).toSubtype) => f (Chapter3.SetTheory.Set.fst p) = Chapter3.SetTheory.Set.snd p

theorem Chapter3.SetTheory.Set.graph_inj [SetTheory] {X Y : Set} (f f' : X.toSubtype → Y.toSubtype) : graph f = graph f' ↔ f = f'

Вправа 3.5.10

theorem Chapter3.SetTheory.Set.is_graph [SetTheory] {X Y G : Set} (hG : G ⊆ X ×ˢ Y) (hvert : ∀ (x : X.toSubtype), ∃! y : Y.toSubtype, OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ G) : ∃! f : X.toSubtype → Y.toSubtype, G = graph f

theorem Chapter3.SetTheory.Set.powerset_axiom' [SetTheory] (X Y : Set) : ∃! S : Set, ∀ (F : Object), F ∈ S ↔ ∃ (f : Y.toSubtype → X.toSubtype), ↑f = F

Вправа 3.5.11. Це тривіально випливає з SetTheory.Set.powerset_axiom, але вправа полягає у виведенні твердження з SetTheory.Set.exists_powerset.

theorem Chapter3.SetTheory.Set.recursion [SetTheory] (X : Set) (f : nat.toSubtype → X.toSubtype → X.toSubtype) (c : X.toSubtype) : ∃! a : nat.toSubtype → X.toSubtype, a 0 = c ∧ ∀ (n : ℕ), a ↑(n + 1) = f (↑n) (a ↑n)

Вправа 3.5.12, з включеними помилками з веб-сайту

theorem Chapter3.SetTheory.Set.nat_unique [SetTheory] (nat' : Set) (zero : nat'.toSubtype) (succ : nat'.toSubtype → nat'.toSubtype) (succ_ne : ∀ (n : nat'.toSubtype), succ n ≠ zero) (succ_of_ne : ∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ m) (ind : ∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P n) : ∃! f : nat.toSubtype → nat'.toSubtype, Function.Bijective f ∧ f 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), f n = n' ↔ f ↑(nat_equiv.symm n + 1) = succ n'

Вправа 3.5.13