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

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

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

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

structure Chapter3.OrderedPair [SetTheory] : Type

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

• 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

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 (Впорядкована пара)

@[reducible, inline]

abbrev 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 ⋯

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.2 (Декартовий добуток)

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 }

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]

abbrev Chapter3.SetTheory.Set.curry [SetTheory] {X Y Z : Set} (f : (X ×ˢ Y).toSubtype → Z.toSubtype) : X.toSubtype → Y.toSubtype → Z.toSubtype

Equations

• Chapter3.SetTheory.Set.curry f x y = f ⟨Chapter3.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) }

@[reducible, inline]

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

Equations

• Chapter3.SetTheory.Set.uncurry f z = f (Chapter3.SetTheory.Set.fst z) (Chapter3.SetTheory.Set.snd z)

theorem Chapter3.SetTheory.Set.curry_uncurry [SetTheory] {X Y Z : Set} (f : X.toSubtype → Y.toSubtype → Z.toSubtype) : curry (uncurry f) = f

theorem Chapter3.SetTheory.Set.uncurry_curry [SetTheory] {X Y Z : Set} (f : (X ×ˢ Y).toSubtype → Z.toSubtype) : uncurry (curry f) = f

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[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-овського добутку множин

Equations

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

@[reducible, inline]

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

Визначення 3.5.7

Equations

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

@[reducible, inline]

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

Визначення 3.5.7

Equations

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

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

Визначення 3.5.7

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

@[simp]

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

@[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.11. Я підозрюю, що більшість еквівалентностей вимагатимуть класичних міркувань і будуть визначені лише необчислювально, але був би радий дізнатися про контрприклади.

Equations

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

@[reducible, inline]

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

Приклад 3.5.11

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 (i : I.toSubtype) => X).toSubtype ≃ (I.toSubtype → X.toSubtype)

Приклад 3.5.11

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

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

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

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

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

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_equiv_Fin [SetTheory] (n : ℕ) : (Fin n).toSubtype ≃ _root_.Fin n

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

Equations

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

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

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

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

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

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

theorem Chapter3.SetTheory.Set.Tuple.ext {inst✝ : SetTheory} {n : ℕ} {x y : Tuple n} (X : x.X = y.X) : HEq x.x y.x → x = y

theorem Chapter3.SetTheory.Set.Tuple.ext_iff {inst✝ : SetTheory} {n : ℕ} {x y : Tuple n} : x = y ↔ x.X = y.X ∧ HEq x.x y.x

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.power_set_axiom' [SetTheory] (X Y : Set) : ∃! S : Set, ∀ (F : Object), F ∈ S ↔ ∃ (f : Y.toSubtype → X.toSubtype), object_of f = F

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

theorem Chapter3.SetTheory.Set.recursion [SetTheory] (X : Type) (f : nat.toSubtype → X → X) (c : X) : ∃! a : nat.toSubtype → X, 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