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

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

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

• Образи чи прообрази (Mathlib-овських) функці, у рамках теорії множин Глави 3.1. (Функції Глави 3.2 відтепер вважаються застарілими та не будуть далі використовуватися.)
• Зв'язок із Mathlib-овськими нотаціями образа f '' S та прообраза f ⁻¹' S.

@[reducible, inline]

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

Визначення 3.4.1. Цікаво, що визначення не вимагає, щоб S було підмножиною X.

Equations

• Chapter3.SetTheory.Set.image f S = X.replace ⋯

theorem Chapter3.SetTheory.Set.mem_image [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (S : Set) (y : Object) : y ∈ image f S ↔ ∃ (x : X.toSubtype), ↑x ∈ S ∧ ↑(f x) = y

Визначення 3.4.1

theorem Chapter3.SetTheory.Set.image_eq_specify [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (S : Set) : image f S = Y.specify fun (y : Y.toSubtype) => ∃ (x : X.toSubtype), ↑x ∈ S ∧ f x = y

Альтернативне визначення зображення використовуючи аксіоми специфікації

theorem Chapter3.SetTheory.Set.image_eq_image [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (S : Set) : {x : Object | x ∈ image f S} = Subtype.val '' (f '' {x : X.toSubtype | ↑x ∈ S})

Зв'язок з поняттям відображення в Mathlib. Зверніть увагу на необхідність використання приведення Subtype.val для забезпечення узгодженості всіх типів.

@[reducible, inline]

abbrev Chapter3.f_3_4_2 [SetTheory] : nat.toSubtype → nat.toSubtype

Приклад 3.4.2

Equations

• Chapter3.f_3_4_2 n = ↑(2 * Chapter3.SetTheory.Set.nat_equiv.symm n)

theorem Chapter3.SetTheory.Set.image_f_3_4_2 [SetTheory] : image f_3_4_2 {1, 2, 3} = {2, 4, 6}

theorem Chapter3.SetTheory.Set.mem_image_of_eval [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (S : Set) (x : X.toSubtype) : ↑x ∈ S → ↑(f x) ∈ image f S

theorem Chapter3.SetTheory.Set.mem_image_of_eval_counter [SetTheory] : ∃ (X : Set) (Y : Set) (f : X.toSubtype → Y.toSubtype) (S : Set) (x : X.toSubtype), ¬(↑(f x) ∈ image f S → ↑x ∈ S)

@[reducible, inline]

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

Визначення 3.4.4 (прообрази). Знову ж таки, не обов'язково, щоб U було підмножиною Y.

Equations

• Chapter3.SetTheory.Set.preimage f U = X.specify fun (x : X.toSubtype) => ↑(f x) ∈ U

theorem Chapter3.SetTheory.Set.mem_preimage [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (U : Set) (x : X.toSubtype) : ↑x ∈ preimage f U ↔ ↑(f x) ∈ U

theorem Chapter3.SetTheory.Set.preimage_eq [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (U : Set) : {x : Object | x ∈ preimage f U} = Subtype.val '' (f ⁻¹' {y : Y.toSubtype | ↑y ∈ U})

Звя'зок із Mathlib-овським поняттям прообразу.

theorem Chapter3.SetTheory.Set.preimage_f_3_4_2 [SetTheory] : preimage f_3_4_2 {2, 4, 6} = {1, 2, 3}

Приклад 3.4.5

theorem Chapter3.SetTheory.Set.image_preimage_f_3_4_2 [SetTheory] : image f_3_4_2 (preimage f_3_4_2 {1, 2, 3}) ≠ {1, 2, 3}

instance Chapter3.SetTheory.Set.inst_pow [SetTheory] : Pow Set Set

Equations

• Chapter3.SetTheory.Set.inst_pow = { pow := Chapter3.SetTheory.pow }

@[reducible, inline]

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

Я не зміг зробити це перетворення через технічну проблему semiOutParam.

Equations

• Chapter3.SetTheory.Set.object_of f = (Chapter3.SetTheory.function_to_object X Y) f

theorem Chapter3.SetTheory.Set.power_set_axiom [SetTheory] {X Y : Set} (F : Object) : F ∈ X ^ Y ↔ ∃ (f : Y.toSubtype → X.toSubtype), object_of f = F

@[reducible, inline]

abbrev Chapter3.f_3_4_8_a [SetTheory] : {4, 7}.toSubtype → {0, 1}.toSubtype

Приклад 3.4.8

Equations

• Chapter3.f_3_4_8_a x = ⟨0, ⋯⟩

@[reducible, inline]

noncomputable abbrev Chapter3.f_3_4_8_b [SetTheory] : {4, 7}.toSubtype → {0, 1}.toSubtype

Equations

• Chapter3.f_3_4_8_b x = if ↑x = 4 then ⟨0, ⋯⟩ else ⟨1, ⋯⟩

@[reducible, inline]

noncomputable abbrev Chapter3.f_3_4_8_c [SetTheory] : {4, 7}.toSubtype → {0, 1}.toSubtype

Equations

• Chapter3.f_3_4_8_c x = if ↑x = 4 then ⟨1, ⋯⟩ else ⟨0, ⋯⟩

@[reducible, inline]

abbrev Chapter3.f_3_4_8_d [SetTheory] : {4, 7}.toSubtype → {0, 1}.toSubtype

Equations

• Chapter3.f_3_4_8_d x = ⟨1, ⋯⟩

theorem Chapter3.SetTheory.Set.example_3_4_8 [SetTheory] (F : Object) : F ∈ {4, 7} ^ {0, 1} ↔ F = object_of f_3_4_8_a ∨ F = object_of f_3_4_8_b ∨ F = object_of f_3_4_8_c ∨ F = object_of f_3_4_8_d

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.powerset [SetTheory] (X : Set) : Set

Лема 3.4.9. Тут потрібно надати відповідне визначення множини потужностей.

Equations

• X.powerset = sorry

theorem Chapter3.SetTheory.Set.mem_powerset [SetTheory] {X : Set} (x : Object) : x ∈ X.powerset ↔ ∃ (Y : Set), x = set_to_object Y ∧ Y ⊆ X

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

Ремарка 3.4.10

theorem Chapter3.SetTheory.Set.union_axiom [SetTheory] (A : Set) (x : Object) : x ∈ union A ↔ ∃ (S : Set), x ∈ S ∧ set_to_object S ∈ A

Аксіома 3.11 (Об'днання)

theorem Chapter3.SetTheory.Set.example_3_4_11 [SetTheory] : union {set_to_object {2, 3}, set_to_object {3, 4}, set_to_object {4, 5}} = {2, 3, 4, 5}

Приклад 3.4.11

theorem Chapter3.SetTheory.Set.union_eq [SetTheory] (A : Set) : {x : Object | x ∈ union A} = ⋃₀ {S : _root_.Set Object | ∃ (S' : Set), S = {x : Object | x ∈ S'} ∧ set_to_object S' ∈ A}

Зв'язок із Mathlib-овським об'єднанням

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.iUnion [SetTheory] (I : Set) (A : I.toSubtype → Set) : Set

Індексоване об'єднання

Equations

• I.iUnion A = Chapter3.SetTheory.union (I.replace ⋯)

theorem Chapter3.SetTheory.Set.mem_iUnion [SetTheory] {I : Set} (A : I.toSubtype → Set) (x : Object) : x ∈ I.iUnion A ↔ ∃ (α : I.toSubtype), x ∈ A α

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.index_example [SetTheory] : {1, 2, 3}.toSubtype → Set

Equations

• Chapter3.SetTheory.Set.index_example i = if ↑i = 1 then {2, 3} else if ↑i = 2 then {3, 4} else {4, 5}

theorem Chapter3.SetTheory.Set.iUnion_example [SetTheory] : {1, 2, 3}.iUnion index_example = {2, 3, 4, 5}

theorem Chapter3.SetTheory.Set.iUnion_eq [SetTheory] (I : Set) (A : I.toSubtype → Set) : {x : Object | x ∈ I.iUnion A} = ⋃ (α : I.toSubtype), {x : Object | x ∈ A α}

Зв'язок із Mathlib-овським індексованим об'єднанням

theorem Chapter3.SetTheory.Set.iUnion_of_empty [SetTheory] (A : ∅.toSubtype → Set) : ∅.iUnion A = ∅

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.nonempty_choose [SetTheory] {I : Set} (hI : I ≠ ∅) : I.toSubtype

Індексований перетин

Equations

• Chapter3.SetTheory.Set.nonempty_choose hI = ⟨⋯.choose, ⋯⟩

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.iInter' [SetTheory] (I : Set) (β : I.toSubtype) (A : I.toSubtype → Set) : Set

Equations

• I.iInter' β A = (A β).specify fun (x : (A β).toSubtype) => ∀ (α : I.toSubtype), ↑x ∈ A α

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iInter [SetTheory] (I : Set) (hI : I ≠ ∅) (A : I.toSubtype → Set) : Set

Equations

• I.iInter hI A = I.iInter' (Chapter3.SetTheory.Set.nonempty_choose hI) A

theorem Chapter3.SetTheory.Set.mem_iInter [SetTheory] {I : Set} (hI : I ≠ ∅) (A : I.toSubtype → Set) (x : Object) : x ∈ I.iInter hI A ↔ ∀ (α : I.toSubtype), x ∈ A α

theorem Chapter3.SetTheory.Set.preimage_eq_image_of_inv [SetTheory] {X Y V : Set} (f : X.toSubtype → Y.toSubtype) (f_inv : Y.toSubtype → X.toSubtype) (hf : Function.LeftInverse f_inv f ∧ Function.RightInverse f_inv f) (hV : V ⊆ Y) : image f_inv V = preimage f V

Вправа 3.4.1

theorem Chapter3.SetTheory.Set.image_of_inter [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (A B : Set) : image f (A ∩ B) ⊆ image f A ∩ image f B

Вправа 3.4.3. Also state and prove an assertion regarding whether ⊆ can be improved to =.

theorem Chapter3.SetTheory.Set.image_of_diff [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (A B : Set) : image f A \ image f B ⊆ image f (A \ B)

theorem Chapter3.SetTheory.Set.image_of_union [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (A B : Set) : image f (A ∪ B) = image f A ∪ image f B

theorem Chapter3.SetTheory.Set.preimage_of_inter [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (A B : Set) : preimage f (A ∩ B) = preimage f A ∩ preimage f B

Вправа 3.4.4

theorem Chapter3.SetTheory.Set.preimage_of_union [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (A B : Set) : preimage f (A ∪ B) = preimage f A ∪ preimage f B

theorem Chapter3.SetTheory.Set.preimage_of_diff [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (A B : Set) : preimage f (A \ B) = preimage f A \ preimage f B

theorem Chapter3.SetTheory.Set.image_preimage_of_surj [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) : (∀ S ⊆ Y, image f (preimage f S) = S) ↔ Function.Surjective f

Вправа 3.4.5

theorem Chapter3.SetTheory.Set.preimage_image_of_inj [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) : (∀ S ⊆ X, preimage f (image f S) = S) ↔ Function.Injective f

Вправа 3.4.5

theorem Chapter3.SetTheory.Set.partial_functions [SetTheory] {X Y : Set} : ∃ (Z : Set), ∀ (F : Object), F ∈ Z ↔ ∃ (X' : Set) (Y' : Set), X' ⊆ X ∧ Y' ⊆ Y ∧ ∃ (f : X'.toSubtype → Y'.toSubtype), F = object_of f

Вправа 3.4.7

theorem Chapter3.SetTheory.Set.union_pair_exists [SetTheory] (X Y : Set) : ∃ (Z : Set), ∀ (x : Object), x ∈ Z ↔ x ∈ X ∨ x ∈ Y

Вправа 3.4.8. Мета цієї вправи - довести її твердження без використання операції попарного об'єднання ∪.

theorem Chapter3.SetTheory.Set.iInter'_insensitive [SetTheory] {I : Set} (β β' : I.toSubtype) (A : I.toSubtype → Set) : I.iInter' β A = I.iInter' β' A

Вправа 3.4.9

theorem Chapter3.SetTheory.Set.union_iUnion [SetTheory] {I J : Set} (A : (I ∪ J).toSubtype → Set) : ((I.iUnion fun (α : I.toSubtype) => A ⟨↑α, ⋯⟩) ∪ J.iUnion fun (α : J.toSubtype) => A ⟨↑α, ⋯⟩) = (I ∪ J).iUnion A

Вправа 3.4.10

theorem Chapter3.SetTheory.Set.union_of_nonempty [SetTheory] {I J : Set} (hI : I ≠ ∅) (hJ : J ≠ ∅) : I ∪ J ≠ ∅

Вправа 3.4.10

theorem Chapter3.SetTheory.Set.inter_iInter [SetTheory] {I J : Set} (hI : I ≠ ∅) (hJ : J ≠ ∅) (A : (I ∪ J).toSubtype → Set) : ((I.iInter hI fun (α : I.toSubtype) => A ⟨↑α, ⋯⟩) ∪ J.iInter hJ fun (α : J.toSubtype) => A ⟨↑α, ⋯⟩) = (I ∪ J).iInter ⋯ A

Вправа 3.4.10

theorem Chapter3.SetTheory.Set.compl_iUnion [SetTheory] {X I : Set} (hI : I ≠ ∅) (A : I.toSubtype → Set) : X \ I.iUnion A = I.iInter hI fun (α : I.toSubtype) => X \ A α

Вправа 3.4.11

theorem Chapter3.SetTheory.Set.compl_iInter [SetTheory] {X I : Set} (hI : I ≠ ∅) (A : I.toSubtype → Set) : X \ I.iInter hI A = I.iUnion fun (α : I.toSubtype) => X \ A α

Вправа 3.4.11