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

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

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

namespace Chapter3export SetTheory (Set Object nat)variable [SetTheory]

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

abbrev SetTheory.Set.image {X Y:Set} (f:X → Y) (S: Set) : Set := X.replace (P := fun x y ↦ y = f x ∧ x.val ∈ S) (inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Set⊢ ∀ (x : X.toSubtype) (y y' : Object), (fun x y => y = ↑(f x) ∧ ↑x ∈ S) x y ∧ (fun x y => y = ↑(f x) ∧ ↑x ∈ S) x y' → y = y' inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Setx:X.toSubtypey:Objecty':Objecthy:(fun x y => y = ↑(f x) ∧ ↑x ∈ S) x yhy':(fun x y => y = ↑(f x) ∧ ↑x ∈ S) x y'⊢ y = y' inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Setx:X.toSubtypey:Objecty':Objecthy:y = ↑(f x) ∧ ↑x ∈ Shy':y' = ↑(f x) ∧ ↑x ∈ S⊢ y = y' All goals completed! 🐙 )

Визначення 3.4.1

theorem SetTheory.Set.mem_image {X Y:Set} (f:X → Y) (S: Set) (y:Object) : y ∈ image f S ↔ ∃ x:X, x.val ∈ S ∧ f x = y := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Sety:Object⊢ y ∈ image f S ↔ ∃ x, ↑x ∈ S ∧ ↑(f x) = y inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Sety:Object⊢ (∃ x, y = ↑(f x) ∧ ↑x ∈ S) ↔ ∃ x, ↑x ∈ S ∧ ↑(f x) = y inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Sety:Object⊢ ∀ (a : X.toSubtype), y = ↑(f a) ∧ ↑a ∈ S ↔ ↑a ∈ S ∧ ↑(f a) = y; inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Sety:Objectx:X.toSubtype⊢ y = ↑(f x) ∧ ↑x ∈ S ↔ ↑x ∈ S ∧ ↑(f x) = y All goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.image_eq_specify {X Y:Set} (f:X → Y) (S: Set) : image f S = Y.specify (fun y ↦ ∃ x:X, x.val ∈ S ∧ f x = y) := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Set⊢ image f S = Y.specify fun y => ∃ x, ↑x ∈ S ∧ f x = y All goals completed! 🐙

Зв'язок з поняттям відображення в Mathlib. Зверніть увагу на необхідність використання приведення Subtype.val.{u} {α : Sort u} {p : α → Prop} (self : Subtype p) : αSubtype.val для забезпечення узгодженості всіх типів.

theorem declaration uses 'sorry'SetTheory.Set.image_eq_image {X Y:Set} (f:X → Y) (S: Set): (image f S: _root_.Set Object) = Subtype.val '' (f '' {x | x.val ∈ S}) := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Set⊢ {x | x ∈ image f S} = Subtype.val '' (f '' {x | ↑x ∈ S}) All goals completed! 🐙

Приклад 3.4.2

abbrev f_3_4_2 : nat → nat := fun n ↦ (2*n:ℕ)
theorem declaration uses 'sorry'SetTheory.Set.image_f_3_4_2 : image f_3_4_2 {1,2,3} = {2,4,6} := inst✝:SetTheory⊢ image f_3_4_2 {1, 2, 3} = {2, 4, 6} All goals completed! 🐙

Приклад 3.4.3 записаний із використанням поняття зображення Mathlib

declaration uses 'sorry'example : (fun n:ℤ ↦ n^2) '' {-1,0,1,2} = {0,1,4} := inst✝:SetTheory⊢ (fun n => n ^ 2) '' {-1, 0, 1, 2} = {0, 1, 4} All goals completed! 🐙
theorem declaration uses 'sorry'SetTheory.Set.mem_image_of_eval {X Y:Set} (f:X → Y) (S: Set) (x:X) : x.val ∈ S → (f x).val ∈ image f S := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Setx:X.toSubtype⊢ ↑x ∈ S → ↑(f x) ∈ image f S All goals completed! 🐙theorem declaration uses 'sorry'SetTheory.Set.mem_image_of_eval_counter : ∃ (X Y:Set) (f:X → Y) (S: Set) (x:X), ¬((f x).val ∈ image f S → x.val ∈ S) := inst✝:SetTheory⊢ ∃ X Y f S x, ¬(↑(f x) ∈ image f S → ↑x ∈ S) All goals completed! 🐙

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

abbrev SetTheory.Set.preimage {X Y:Set} (f:X → Y) (U: Set) : Set := X.specify (P := fun x ↦ (f x).val ∈ U)
theorem SetTheory.Set.mem_preimage {X Y:Set} (f:X → Y) (U: Set) (x:X) : x.val ∈ preimage f U ↔ (f x).val ∈ U := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:X.toSubtype⊢ ↑x ∈ preimage f U ↔ ↑(f x) ∈ U All goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.preimage_eq {X Y:Set} (f:X → Y) (U: Set) : ((preimage f U): _root_.Set Object) = Subtype.val '' (f⁻¹' {y | y.val ∈ U}) := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Set⊢ {x | x ∈ preimage f U} = Subtype.val '' (f ⁻¹' {y | ↑y ∈ U}) All goals completed! 🐙

Приклад 3.4.5

theorem declaration uses 'sorry'SetTheory.Set.preimage_f_3_4_2 : preimage f_3_4_2 {2,4,6} = {1,2,3} := inst✝:SetTheory⊢ preimage f_3_4_2 {2, 4, 6} = {1, 2, 3} All goals completed! 🐙
theorem declaration uses 'sorry'SetTheory.Set.image_preimage_f_3_4_2 : image f_3_4_2 (preimage f_3_4_2 {1,2,3}) ≠ {1,2,3} := inst✝:SetTheory⊢ image f_3_4_2 (preimage f_3_4_2 {1, 2, 3}) ≠ {1, 2, 3} All goals completed! 🐙

Приклад 3.4.6 (використовуючи Mathlib-овську нотацію прообраза)

declaration uses 'sorry'example : (fun n:ℤ ↦ n^2) ⁻¹' {0,1,4} = {-2,-1,0,1,2} := inst✝:SetTheory⊢ (fun n => n ^ 2) ⁻¹' {0, 1, 4} = {-2, -1, 0, 1, 2} All goals completed! 🐙
declaration uses 'sorry'example : (fun n:ℤ ↦ n^2) ⁻¹' ((fun n:ℤ ↦ n^2) '' {-1,0,1,2}) ≠ {-1,0,1,2} := inst✝:SetTheory⊢ (fun n => n ^ 2) ⁻¹' ((fun n => n ^ 2) '' {-1, 0, 1, 2}) ≠ {-1, 0, 1, 2} All goals completed! 🐙instance SetTheory.Set.inst_pow : Pow Set Set where pow := SetTheory.pow

Я не зміг зробити це перетворення через технічну проблему semiOutParam.{u} (α : Sort u) : Sort usemiOutParam.

abbrev SetTheory.Set.object_of {X Y:Set} (f: X → Y) : Object := function_to_object X Y f
theorem SetTheory.Set.power_set_axiom {X Y:Set} (F:Object) : F ∈ (X ^ Y) ↔ ∃ f: Y → X, object_of f = F := SetTheory.power_set_axiom X Y F

Приклад 3.4.8

abbrev f_3_4_8_a : ({4,7}:Set) → ({0,1}:Set) := fun x ↦ ⟨ 0, inst✝:SetTheoryx:{4, 7}.toSubtype⊢ 0 ∈ {0, 1} All goals completed! 🐙 ⟩
open Classical in noncomputable abbrev f_3_4_8_b : ({4,7}:Set) → ({0,1}:Set) := fun x ↦ if x.val = 4 then ⟨ 0, inst✝:SetTheoryx:{4, 7}.toSubtype⊢ 0 ∈ {0, 1} All goals completed! 🐙 ⟩ else ⟨ 1, inst✝:SetTheoryx:{4, 7}.toSubtype⊢ 1 ∈ {0, 1} All goals completed! 🐙 ⟩open Classical in noncomputable abbrev f_3_4_8_c : ({4,7}:Set) → ({0,1}:Set) := fun x ↦ if x.val = 4 then ⟨ 1, inst✝:SetTheoryx:{4, 7}.toSubtype⊢ 1 ∈ {0, 1} All goals completed! 🐙 ⟩ else ⟨ 0, inst✝:SetTheoryx:{4, 7}.toSubtype⊢ 0 ∈ {0, 1} All goals completed! 🐙 ⟩abbrev f_3_4_8_d : ({4,7}:Set) → ({0,1}:Set) := fun x ↦ ⟨ 1, inst✝:SetTheoryx:{4, 7}.toSubtype⊢ 1 ∈ {0, 1} All goals completed! 🐙 ⟩theorem declaration uses 'sorry'SetTheory.Set.example_3_4_8 (F:Object) : F ∈ ({4,7}:Set) ^ ({0,1}:Set) ↔ 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 := inst✝:SetTheoryF: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 All goals completed! 🐙

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

abbrev declaration uses 'sorry'SetTheory.Set.powerset (X:Set) : Set := sorry
theorem declaration uses 'sorry'SetTheory.Set.mem_powerset {X:Set} (x:Object) : x ∈ powerset X ↔ ∃ Y:Set, x = Y ∧ Y ⊆ X := inst✝:SetTheoryX:Setx:Object⊢ x ∈ X.powerset ↔ ∃ Y, x = set_to_object Y ∧ Y ⊆ X All goals completed! 🐙

Ремарка 3.4.10

theorem declaration uses 'sorry'SetTheory.Set.powerset_of_triple (a b c x:Object) : x ∈ powerset {a,b,c} ↔ x = (∅:Set) ∨ x = ({a}:Set) ∨ x = ({b}:Set) ∨ x = ({c}:Set) ∨ x = ({a,b}:Set) ∨ x = ({a,c}:Set) ∨ x = ({b,c}:Set) ∨ x = ({a,b,c}:Set) := inst✝:SetTheorya:Objectb:Objectc:Objectx: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} All goals completed! 🐙

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

theorem SetTheory.Set.union_axiom (A: Set) (x:Object) : x ∈ union A ↔ ∃ (S:Set), x ∈ S ∧ (S:Object) ∈ A := SetTheory.union_axiom A x

Приклад 3.4.11

theorem declaration uses 'sorry'SetTheory.Set.example_3_4_11 : union { (({2,3}:Set):Object), (({3,4}:Set):Object), (({4,5}:Set):Object) } = {2,3,4,5} := inst✝:SetTheory⊢ union {set_to_object {2, 3}, set_to_object {3, 4}, set_to_object {4, 5}} = {2, 3, 4, 5} All goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_eq (A: Set) : (union A : _root_.Set Object) = ⋃₀ { S : _root_.Set Object | ∃ S':Set, S = S' ∧ (S':Object) ∈ A } := inst✝:SetTheoryA:Set⊢ {x | x ∈ union A} = ⋃₀ {S | ∃ S', S = {x | x ∈ S'} ∧ set_to_object S' ∈ A} All goals completed! 🐙

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

abbrev SetTheory.Set.iUnion (I: Set) (A: I → Set) : Set := union (I.replace (P := fun α S ↦ S = A α) (inst✝:SetTheoryI:SetA:I.toSubtype → Set⊢ ∀ (x : I.toSubtype) (y y' : Object), (fun α S => S = set_to_object (A α)) x y ∧ (fun α S => S = set_to_object (A α)) x y' → y = y' inst✝:SetTheoryI:SetA:I.toSubtype → Setx:I.toSubtypey:Objecty':Objecth1:(fun α S => S = set_to_object (A α)) x yh2:(fun α S => S = set_to_object (A α)) x y'⊢ y = y'; inst✝:SetTheoryI:SetA:I.toSubtype → Setx:I.toSubtypey:Objecty':Objecth1:y = set_to_object (A x)h2:y' = set_to_object (A x)⊢ y = y'; All goals completed! 🐙))
theorem SetTheory.Set.mem_iUnion {I:Set} (A: I → Set) (x:Object) : x ∈ iUnion I A ↔ ∃ α:I, x ∈ A α := inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Object⊢ x ∈ I.iUnion A ↔ ∃ α, x ∈ A α inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Object⊢ (∃ S, x ∈ S ∧ set_to_object S ∈ I.replace ⋯) ↔ ∃ α, x ∈ A α inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Object⊢ (∃ S, x ∈ S ∧ set_to_object S ∈ I.replace ⋯) → ∃ α, x ∈ A αinst✝:SetTheoryI:SetA:I.toSubtype → Setx:Object⊢ (∃ α, x ∈ A α) → ∃ S, x ∈ S ∧ set_to_object S ∈ I.replace ⋯ inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Object⊢ (∃ S, x ∈ S ∧ set_to_object S ∈ I.replace ⋯) → ∃ α, x ∈ A α inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Objecth:∃ S, x ∈ S ∧ set_to_object S ∈ I.replace ⋯⊢ ∃ α, x ∈ A α inst✝:SetTheoryI:SetA:I.toSubtype → Setx:ObjectS:Sethx:x ∈ ShS:set_to_object S ∈ I.replace ⋯⊢ ∃ α, x ∈ A α inst✝:SetTheoryI:SetA:I.toSubtype → Setx:ObjectS:Sethx:x ∈ ShS:∃ x, set_to_object S = set_to_object (A x)⊢ ∃ α, x ∈ A α inst✝:SetTheoryI:SetA:I.toSubtype → Setx:ObjectS:Sethx:x ∈ Sα:I.toSubtypehα:set_to_object S = set_to_object (A α)⊢ ∃ α, x ∈ A α inst✝:SetTheoryI:SetA:I.toSubtype → Setx:ObjectS:Sethx:x ∈ Sα:I.toSubtypehα:S = A α⊢ ∃ α, x ∈ A α inst✝:SetTheoryI:SetA:I.toSubtype → Setx:ObjectS:Setα:I.toSubtypehx:x ∈ A αhα:S = A α⊢ ∃ α, x ∈ A α All goals completed! 🐙 inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Objecth:∃ α, x ∈ A α⊢ ∃ S, x ∈ S ∧ set_to_object S ∈ I.replace ⋯ inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Objectα:I.toSubtypehx:x ∈ A α⊢ ∃ S, x ∈ S ∧ set_to_object S ∈ I.replace ⋯ inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Objectα:I.toSubtypehx:x ∈ A α⊢ x ∈ A α ∧ set_to_object (A α) ∈ I.replace ⋯ inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Objectα:I.toSubtypehx:x ∈ A α⊢ x ∈ A αinst✝:SetTheoryI:SetA:I.toSubtype → Setx:Objectα:I.toSubtypehx:x ∈ A α⊢ set_to_object (A α) ∈ I.replace ⋯ inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Objectα:I.toSubtypehx:x ∈ A α⊢ x ∈ A α All goals completed! 🐙 inst✝:SetTheoryI:SetA:I.toSubtype → Setx:Objectα:I.toSubtypehx:x ∈ A α⊢ ∃ x, set_to_object (A α) = set_to_object (A x) All goals completed! 🐙open Classical in noncomputable abbrev SetTheory.Set.index_example : ({1,2,3}:Set) → Set := fun i ↦ if i.val = 1 then {2,3} else if i.val = 2 then {3,4} else {4,5}theorem declaration uses 'sorry'SetTheory.Set.iUnion_example : iUnion {1,2,3} index_example = {2,3,4,5} := inst✝:SetTheory⊢ {1, 2, 3}.iUnion index_example = {2, 3, 4, 5} All goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.iUnion_eq (I: Set) (A: I → Set) : (iUnion I A : _root_.Set Object) = ⋃ α, (A α: _root_.Set Object) := inst✝:SetTheoryI:SetA:I.toSubtype → Set⊢ {x | x ∈ I.iUnion A} = ⋃ α, {x | x ∈ A α} All goals completed! 🐙
theorem declaration uses 'sorry'SetTheory.Set.iUnion_of_empty (A: (∅:Set) → Set) : iUnion (∅:Set) A = ∅ := inst✝:SetTheoryA:∅.toSubtype → Set⊢ ∅.iUnion A = ∅ All goals completed! 🐙

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

noncomputable abbrev SetTheory.Set.nonempty_choose {I:Set} (hI: I ≠ ∅) : I := ⟨(nonempty_def hI).choose, (nonempty_def hI).choose_spec⟩
abbrev SetTheory.Set.iInter' (I:Set) (β:I) (A: I → Set) : Set := (A β).specify (P := fun x ↦ ∀ α:I, x.val ∈ A α)noncomputable abbrev SetTheory.Set.iInter (I: Set) (hI: I ≠ ∅) (A: I → Set) : Set := iInter' I (nonempty_choose hI) Atheorem declaration uses 'sorry'SetTheory.Set.mem_iInter {I:Set} (hI: I ≠ ∅) (A: I → Set) (x:Object) : x ∈ iInter I hI A ↔ ∀ α:I, x ∈ A α := inst✝:SetTheoryI:SethI:I ≠ ∅A:I.toSubtype → Setx:Object⊢ x ∈ I.iInter hI A ↔ ∀ (α : I.toSubtype), x ∈ A α All goals completed! 🐙

Вправа 3.4.1

theorem declaration uses 'sorry'SetTheory.Set.preimage_eq_image_of_inv {X Y V:Set} (f:X → Y) (f_inv: Y → X) (hf: Function.LeftInverse f_inv f ∧ Function.RightInverse f_inv f) (hV: V ⊆ Y) : image f_inv V = preimage f V := inst✝:SetTheoryX:SetY:SetV:Setf:X.toSubtype → Y.toSubtypef_inv:Y.toSubtype → X.toSubtypehf:Function.LeftInverse f_inv f ∧ Function.RightInverse f_inv fhV:V ⊆ Y⊢ image f_inv V = preimage f V All goals completed! 🐙
/- Вправа 3.4.2. Сформулюйте та доведіть твердження, що пов'язує `preimage (image f S)` та `S`. -/ -- theorem SetTheory.Set.preimage_of_image {X Y:Set} (f:X → Y) (S: Set) : sorry := by sorry /- Вправа 3.4.2. Сформулюйте та доведіть твердження, що пов'язує `image (preimage f U)` та `U`. -/ -- theorem SetTheory.Set.preimage_of_image {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry

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

theorem declaration uses 'sorry'SetTheory.Set.image_of_inter {X Y:Set} (f:X → Y) (A B: Set) : image f (A ∩ B) ⊆ (image f A) ∩ (image f B) := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeA:SetB:Set⊢ image f (A ∩ B) ⊆ image f A ∩ image f B All goals completed! 🐙
theorem declaration uses 'sorry'SetTheory.Set.image_of_diff {X Y:Set} (f:X → Y) (A B: Set) : (image f A) \ (image f B) ⊆ image f (A \ B) := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeA:SetB:Set⊢ image f A \ image f B ⊆ image f (A \ B) All goals completed! 🐙theorem declaration uses 'sorry'SetTheory.Set.image_of_union {X Y:Set} (f:X → Y) (A B: Set) : image f (A ∪ B) = (image f A) ∪ (image f B) := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeA:SetB:Set⊢ image f (A ∪ B) = image f A ∪ image f B All goals completed! 🐙

Вправа 3.4.4

theorem declaration uses 'sorry'SetTheory.Set.preimage_of_inter {X Y:Set} (f:X → Y) (A B: Set) : preimage f (A ∩ B) = (preimage f A) ∩ (preimage f B) := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeA:SetB:Set⊢ preimage f (A ∩ B) = preimage f A ∩ preimage f B All goals completed! 🐙
theorem declaration uses 'sorry'SetTheory.Set.preimage_of_union {X Y:Set} (f:X → Y) (A B: Set) : preimage f (A ∪ B) = (preimage f A) ∪ (preimage f B) := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeA:SetB:Set⊢ preimage f (A ∪ B) = preimage f A ∪ preimage f B All goals completed! 🐙theorem declaration uses 'sorry'SetTheory.Set.preimage_of_diff {X Y:Set} (f:X → Y) (A B: Set) : preimage f (A \ B) = (preimage f A) \ (preimage f B) := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeA:SetB:Set⊢ preimage f (A \ B) = preimage f A \ preimage f B All goals completed! 🐙

Вправа 3.4.5

theorem declaration uses 'sorry'SetTheory.Set.image_preimage_of_surj {X Y:Set} (f:X → Y) : (∀ S, S ⊆ Y → image f (preimage f S) = S) ↔ Function.Surjective f := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtype⊢ (∀ S ⊆ Y, image f (preimage f S) = S) ↔ Function.Surjective f All goals completed! 🐙

Вправа 3.4.5

theorem declaration uses 'sorry'SetTheory.Set.preimage_image_of_inj {X Y:Set} (f:X → Y) : (∀ S, S ⊆ X → preimage f (image f S) = S) ↔ Function.Injective f := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtype⊢ (∀ S ⊆ X, preimage f (image f S) = S) ↔ Function.Injective f All goals completed! 🐙

Вправа 3.4.7

theorem declaration uses 'sorry'SetTheory.Set.partial_functions {X Y:Set} : ∃ Z:Set, ∀ F:Object, F ∈ Z ↔ ∃ X' Y':Set, X' ⊆ X ∧ Y' ⊆ Y ∧ ∃ f: X' → Y', F = object_of f := inst✝:SetTheoryX:SetY:Set⊢ ∃ Z, ∀ (F : Object), F ∈ Z ↔ ∃ X' Y', X' ⊆ X ∧ Y' ⊆ Y ∧ ∃ f, F = object_of f All goals completed! 🐙

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

theorem declaration uses 'sorry'SetTheory.Set.union_pair_exists (X Y:Set) : ∃ Z:Set, ∀ x, x ∈ Z ↔ (x ∈ X ∨ x ∈ Y) := inst✝:SetTheoryX:SetY:Set⊢ ∃ Z, ∀ (x : Object), x ∈ Z ↔ x ∈ X ∨ x ∈ Y All goals completed! 🐙

Вправа 3.4.9

theorem declaration uses 'sorry'SetTheory.Set.iInter'_insensitive {I:Set} (β β':I) (A: I → Set) : iInter' I β A = iInter' I β' A := inst✝:SetTheoryI:Setβ:I.toSubtypeβ':I.toSubtypeA:I.toSubtype → Set⊢ I.iInter' β A = I.iInter' β' A All goals completed! 🐙

Вправа 3.4.10

theorem declaration uses 'sorry'SetTheory.Set.union_iUnion {I J:Set} (A: (I ∪ J:Set) → Set) : iUnion I (fun α ↦ A ⟨ α.val, inst✝:SetTheoryI:SetJ:SetA:(I ∪ J).toSubtype → Setα:I.toSubtype⊢ ↑α ∈ I ∪ J All goals completed! 🐙⟩) ∪ iUnion J (fun α ↦ A ⟨ α.val, inst✝:SetTheoryI:SetJ:SetA:(I ∪ J).toSubtype → Setα:J.toSubtype⊢ ↑α ∈ I ∪ J All goals completed! 🐙⟩) = iUnion (I ∪ J) A := inst✝:SetTheoryI:SetJ:SetA:(I ∪ J).toSubtype → Set⊢ ((I.iUnion fun α => A ⟨↑α, ⋯⟩) ∪ J.iUnion fun α => A ⟨↑α, ⋯⟩) = (I ∪ J).iUnion A All goals completed! 🐙

Вправа 3.4.10

theorem declaration uses 'sorry'SetTheory.Set.union_of_nonempty {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) : I ∪ J ≠ ∅ := inst✝:SetTheoryI:SetJ:SethI:I ≠ ∅hJ:J ≠ ∅⊢ I ∪ J ≠ ∅ All goals completed! 🐙

Вправа 3.4.10

theorem declaration uses 'sorry'SetTheory.Set.inter_iInter {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) (A: (I ∪ J:Set) → Set) : iInter I hI (fun α ↦ A ⟨ α.val, inst✝:SetTheoryI:SetJ:SethI:I ≠ ∅hJ:J ≠ ∅A:(I ∪ J).toSubtype → Setα:I.toSubtype⊢ ↑α ∈ I ∪ J All goals completed! 🐙⟩) ∪ iInter J hJ (fun α ↦ A ⟨ α.val, inst✝:SetTheoryI:SetJ:SethI:I ≠ ∅hJ:J ≠ ∅A:(I ∪ J).toSubtype → Setα:J.toSubtype⊢ ↑α ∈ I ∪ J All goals completed! 🐙⟩) = iInter (I ∪ J) (union_of_nonempty hI hJ) A := inst✝:SetTheoryI:SetJ:SethI:I ≠ ∅hJ:J ≠ ∅A:(I ∪ J).toSubtype → Set⊢ ((I.iInter hI fun α => A ⟨↑α, ⋯⟩) ∪ J.iInter hJ fun α => A ⟨↑α, ⋯⟩) = (I ∪ J).iInter ⋯ A All goals completed! 🐙

Вправа 3.4.11

theorem declaration uses 'sorry'SetTheory.Set.compl_iUnion {X I: Set} (hI: I ≠ ∅) (A: I → Set) : X \ iUnion I A = iInter I hI (fun α ↦ X \ A α) := inst✝:SetTheoryX:SetI:SethI:I ≠ ∅A:I.toSubtype → Set⊢ X \ I.iUnion A = I.iInter hI fun α => X \ A α All goals completed! 🐙

Вправа 3.4.11

theorem declaration uses 'sorry'SetTheory.Set.compl_iInter {X I: Set} (hI: I ≠ ∅) (A: I → Set) : X \ iInter I hI A = iUnion I (fun α ↦ X \ A α) := inst✝:SetTheoryX:SetI:SethI:I ≠ ∅A:I.toSubtype → Set⊢ X \ I.iInter hI A = I.iUnion fun α => X \ A α All goals completed! 🐙
end Chapter3