1. Analysis
  2. 3.4. Images and inverse images
Imports
import Mathlib.Tactic import Analysis.Section_3_1

Analysis I, Section 3.4: Images and inverse images

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

  • Images and inverse images of (Mathlib) functions, within the framework of Section 3.1 set theory. (The Section 3.3 functions are now deprecated and will not be used further.)

  • Connection with Mathlib's image f '' S and preimage f ⁻¹' S notions.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

  • (Add tip here)

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

Definition 3.4.1. Interestingly, the definition does not require S to be a subset of X.

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

Definition 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 All goals completed! 🐙

Alternate definition of image using axiom of specification

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

Connection with Mathlib's notion of image. Note the need to utilize the Subtype.­val coercion to make everything type consistent.

theorem 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}) inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Setx✝:Object⊢ x✝ ∈ {x | x ∈ image f S} ↔ x✝ ∈ Subtype.val '' (f '' {x | ↑x ∈ S}); inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Setx✝:Object⊢ (∃ a, (∃ (x : a ∈ X), ↑(f ⟨a, ⋯⟩) = x✝) ∧ a ∈ S) ↔ ∃ (x : x✝ ∈ Y), ∃ a ∈ S, ∃ (x_1 : a ∈ X), f ⟨a, ⋯⟩ = ⟨x✝, ⋯⟩; All goals completed! 🐙
theorem SetTheory.Set.image_in_codomain {X Y:Set} (f:X → Y) (S: Set) : image f S ⊆ Y := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Set⊢ image f S ⊆ Y intro _ inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Setx✝:Objecth:x✝ ∈ image f S⊢ x✝ ∈ Y; inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeS:Setx✝:Objecth:∃ x, ↑x ∈ S ∧ ↑(f x) = x✝⊢ x✝ ∈ Y; All goals completed! 🐙

Example 3.4.2

abbrev f_3_4_2 : nat → nat := fun n ↦ (2*n:ℕ)
theorem 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} inst✝:SetTheoryx✝:Object⊢ x✝ ∈ image f_3_4_2 {1, 2, 3} ↔ x✝ ∈ {2, 4, 6}; inst✝:SetTheoryx✝:Object⊢ (∃ x, (↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3) ∧ ↑↑(2 * nat_equiv.symm x) = x✝) ↔ x✝ = 2 ∨ x✝ = 4 ∨ x✝ = 6 inst✝:SetTheoryx✝:Object⊢ (∃ x, (↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3) ∧ ↑↑(2 * nat_equiv.symm x) = x✝) → x✝ = 2 ∨ x✝ = 4 ∨ x✝ = 6inst✝:SetTheoryx✝:Object⊢ x✝ = 2 ∨ x✝ = 4 ∨ x✝ = 6 → ∃ x, (↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3) ∧ ↑↑(2 * nat_equiv.symm x) = x✝ inst✝:SetTheoryx✝:Object⊢ (∃ x, (↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3) ∧ ↑↑(2 * nat_equiv.symm x) = x✝) → x✝ = 2 ∨ x✝ = 4 ∨ x✝ = 6 inst✝:SetTheoryw✝:nat.toSubtypeh✝:↑w✝ = 1⊢ ↑↑(2 * nat_equiv.symm w✝) = 2 ∨ ↑↑(2 * nat_equiv.symm w✝) = 4 ∨ ↑↑(2 * nat_equiv.symm w✝) = 6inst✝:SetTheoryw✝:nat.toSubtypeh✝:↑w✝ = 2⊢ ↑↑(2 * nat_equiv.symm w✝) = 2 ∨ ↑↑(2 * nat_equiv.symm w✝) = 4 ∨ ↑↑(2 * nat_equiv.symm w✝) = 6inst✝:SetTheoryw✝:nat.toSubtypeh✝:↑w✝ = 3⊢ ↑↑(2 * nat_equiv.symm w✝) = 2 ∨ ↑↑(2 * nat_equiv.symm w✝) = 4 ∨ ↑↑(2 * nat_equiv.symm w✝) = 6 inst✝:SetTheoryw✝:nat.toSubtypeh✝:↑w✝ = 1⊢ ↑↑(2 * nat_equiv.symm w✝) = 2 ∨ ↑↑(2 * nat_equiv.symm w✝) = 4 ∨ ↑↑(2 * nat_equiv.symm w✝) = 6inst✝:SetTheoryw✝:nat.toSubtypeh✝:↑w✝ = 2⊢ ↑↑(2 * nat_equiv.symm w✝) = 2 ∨ ↑↑(2 * nat_equiv.symm w✝) = 4 ∨ ↑↑(2 * nat_equiv.symm w✝) = 6inst✝:SetTheoryw✝:nat.toSubtypeh✝:↑w✝ = 3⊢ ↑↑(2 * nat_equiv.symm w✝) = 2 ∨ ↑↑(2 * nat_equiv.symm w✝) = 4 ∨ ↑↑(2 * nat_equiv.symm w✝) = 6 All goals completed! 🐙 inst✝:SetTheoryx✝:Objecth✝:x✝ = 2⊢ ∃ x, (↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3) ∧ ↑↑(2 * nat_equiv.symm x) = x✝inst✝:SetTheoryx✝:Objecth✝:x✝ = 4⊢ ∃ x, (↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3) ∧ ↑↑(2 * nat_equiv.symm x) = x✝inst✝:SetTheoryx✝:Objecth✝:x✝ = 6⊢ ∃ x, (↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3) ∧ ↑↑(2 * nat_equiv.symm x) = x✝; map_tacs [inst✝:SetTheoryx✝:Objecth✝:x✝ = 2⊢ (↑1 = 1 ∨ ↑1 = 2 ∨ ↑1 = 3) ∧ ↑↑(2 * nat_equiv.symm 1) = x✝; inst✝:SetTheoryx✝:Objecth✝:x✝ = 4⊢ (↑2 = 1 ∨ ↑2 = 2 ∨ ↑2 = 3) ∧ ↑↑(2 * nat_equiv.symm 2) = x✝; inst✝:SetTheoryx✝:Objecth✝:x✝ = 6⊢ (↑3 = 1 ∨ ↑3 = 2 ∨ ↑3 = 3) ∧ ↑↑(2 * nat_equiv.symm 3) = x✝] all_goals All goals completed! 🐙/-- Example 3.4.3 is written using Mathlib's notion of image. -/ 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! 🐙

Definition 3.4.4 (inverse images). Again, it is not required that U be a subset of Y.

abbrev SetTheory.Set.preimage {X Y:Set} (f:X → Y) (U: Set) : Set := X.specify (P := fun x ↦ (f x).val ∈ U)
@[simp] 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! 🐙

A version of mem_preimage that does not require x to be of type X.

theorem SetTheory.Set.mem_preimage' {X Y:Set} (f:X → Y) (U: Set) (x:Object) : x ∈ preimage f U ↔ ∃ x': X, x'.val = x ∧ (f x').val ∈ U := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Object⊢ x ∈ preimage f U ↔ ∃ x', ↑x' = x ∧ ↑(f x') ∈ U inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Object⊢ x ∈ preimage f U → ∃ x', ↑x' = x ∧ ↑(f x') ∈ Uinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Object⊢ (∃ x', ↑x' = x ∧ ↑(f x') ∈ U) → x ∈ preimage f U inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Object⊢ x ∈ preimage f U → ∃ x', ↑x' = x ∧ ↑(f x') ∈ U inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Objecth:x ∈ preimage f U⊢ ∃ x', ↑x' = x ∧ ↑(f x') ∈ U; inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Objecth:x ∈ preimage f Uhx:x ∈ X⊢ ∃ x', ↑x' = x ∧ ↑(f x') ∈ Uinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Objecth:x ∈ preimage f Uhx:x ∉ X⊢ ∃ x', ↑x' = x ∧ ↑(f x') ∈ U inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Objecth:x ∈ preimage f Uhx:x ∈ X⊢ ∃ x', ↑x' = x ∧ ↑(f x') ∈ U inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Objecth:x ∈ preimage f Uhx:x ∈ X⊢ ↑⟨x, hx⟩ = x ∧ ↑(f ⟨x, hx⟩) ∈ U; inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Objecth:x ∈ preimage f Uhx:x ∈ Xthis:↑⟨x, hx⟩ ∈ preimage f U ↔ ↑(f ⟨x, hx⟩) ∈ U⊢ ↑⟨x, hx⟩ = x ∧ ↑(f ⟨x, hx⟩) ∈ U; All goals completed! 🐙 inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Objecth:x ∈ preimage f Uhx:x ∉ X⊢ ∃ x', ↑x' = x ∧ ↑(f x') ∈ U All goals completed! 🐙 inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx:Object⊢ (∃ x', ↑x' = x ∧ ↑(f x') ∈ U) → x ∈ preimage f U inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx':X.toSubtypehfx':↑(f x') ∈ U⊢ ↑x' ∈ preimage f U; rwa [mem_preimageinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx':X.toSubtypehfx':↑(f x') ∈ U⊢ ↑(f x') ∈ U

Connection with Mathlib's notion of preimage.

theorem 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}) inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx✝:Object⊢ x✝ ∈ {x | x ∈ preimage f U} ↔ x✝ ∈ Subtype.val '' (f ⁻¹' {y | ↑y ∈ U}); All goals completed! 🐙
theorem SetTheory.Set.preimage_in_domain {X Y:Set} (f:X → Y) (U: Set) : (preimage f U) ⊆ X := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Set⊢ preimage f U ⊆ X intro _ inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeU:Setx✝:Objecta✝:x✝ ∈ preimage f U⊢ x✝ ∈ X; All goals completed! 🐙

Example 3.4.6

theorem 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} inst✝:SetTheoryx✝:Object⊢ x✝ ∈ preimage f_3_4_2 {2, 4, 6} ↔ x✝ ∈ {1, 2, 3}; inst✝:SetTheoryx✝:Object⊢ (∃ x', ↑x' = x✝ ∧ (↑↑(2 * nat_equiv.symm x') = 2 ∨ ↑↑(2 * nat_equiv.symm x') = 4 ∨ ↑↑(2 * nat_equiv.symm x') = 6)) ↔ x✝ = 1 ∨ x✝ = 2 ∨ x✝ = 3; inst✝:SetTheoryx✝:Object⊢ (∃ x', ↑x' = x✝ ∧ (↑↑(2 * nat_equiv.symm x') = 2 ∨ ↑↑(2 * nat_equiv.symm x') = 4 ∨ ↑↑(2 * nat_equiv.symm x') = 6)) → x✝ = 1 ∨ x✝ = 2 ∨ x✝ = 3inst✝:SetTheoryx✝:Object⊢ x✝ = 1 ∨ x✝ = 2 ∨ x✝ = 3 → ∃ x', ↑x' = x✝ ∧ (↑↑(2 * nat_equiv.symm x') = 2 ∨ ↑↑(2 * nat_equiv.symm x') = 4 ∨ ↑↑(2 * nat_equiv.symm x') = 6) inst✝:SetTheoryx✝:Object⊢ (∃ x', ↑x' = x✝ ∧ (↑↑(2 * nat_equiv.symm x') = 2 ∨ ↑↑(2 * nat_equiv.symm x') = 4 ∨ ↑↑(2 * nat_equiv.symm x') = 6)) → x✝ = 1 ∨ x✝ = 2 ∨ x✝ = 3 inst✝:SetTheoryx:nat.toSubtypeh✝:↑↑(2 * nat_equiv.symm x) = 2⊢ ↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3inst✝:SetTheoryx:nat.toSubtypeh✝:↑↑(2 * nat_equiv.symm x) = 4⊢ ↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3inst✝:SetTheoryx:nat.toSubtypeh✝:↑↑(2 * nat_equiv.symm x) = 6⊢ ↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3 inst✝:SetTheoryx:nat.toSubtypeh✝:↑↑(2 * nat_equiv.symm x) = 2⊢ ↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3inst✝:SetTheoryx:nat.toSubtypeh✝:↑↑(2 * nat_equiv.symm x) = 4⊢ ↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3inst✝:SetTheoryx:nat.toSubtypeh✝:↑↑(2 * nat_equiv.symm x) = 6⊢ ↑x = 1 ∨ ↑x = 2 ∨ ↑x = 3 inst✝:SetTheoryx:nat.toSubtypeh✝:2 * nat_equiv.symm x = 6⊢ nat_equiv.symm x = 1 ∨ nat_equiv.symm x = 2 ∨ nat_equiv.symm x = 3 inst✝:SetTheoryx:nat.toSubtypeh✝:2 * nat_equiv.symm x = 4⊢ nat_equiv.symm x = 1 ∨ nat_equiv.symm x = 2 ∨ nat_equiv.symm x = 3inst✝:SetTheoryx:nat.toSubtypeh✝:2 * nat_equiv.symm x = 6⊢ nat_equiv.symm x = 1 ∨ nat_equiv.symm x = 2 ∨ nat_equiv.symm x = 3 All goals completed! 🐙 inst✝:SetTheory⊢ ∃ x', ↑x' = 1 ∧ (↑↑(2 * nat_equiv.symm x') = 2 ∨ ↑↑(2 * nat_equiv.symm x') = 4 ∨ ↑↑(2 * nat_equiv.symm x') = 6)inst✝:SetTheory⊢ ∃ x', ↑x' = 2 ∧ (↑↑(2 * nat_equiv.symm x') = 2 ∨ ↑↑(2 * nat_equiv.symm x') = 4 ∨ ↑↑(2 * nat_equiv.symm x') = 6)inst✝:SetTheory⊢ ∃ x', ↑x' = 3 ∧ (↑↑(2 * nat_equiv.symm x') = 2 ∨ ↑↑(2 * nat_equiv.symm x') = 4 ∨ ↑↑(2 * nat_equiv.symm x') = 6); map_tacs [inst✝:SetTheory⊢ ↑1 = 1 ∧ (↑↑(2 * nat_equiv.symm 1) = 2 ∨ ↑↑(2 * nat_equiv.symm 1) = 4 ∨ ↑↑(2 * nat_equiv.symm 1) = 6); inst✝:SetTheory⊢ ↑2 = 2 ∧ (↑↑(2 * nat_equiv.symm 2) = 2 ∨ ↑↑(2 * nat_equiv.symm 2) = 4 ∨ ↑↑(2 * nat_equiv.symm 2) = 6); inst✝:SetTheory⊢ ↑3 = 3 ∧ (↑↑(2 * nat_equiv.symm 3) = 2 ∨ ↑↑(2 * nat_equiv.symm 3) = 4 ∨ ↑↑(2 * nat_equiv.symm 3) = 6)] all_goals 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! 🐙/-- Example 3.4.7 (using the Mathlib notion of preimage) -/ 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} inst✝:SetTheoryx✝:ℤ⊢ x✝ ∈ (fun n ↦ n ^ 2) ⁻¹' {0, 1, 4} ↔ x✝ ∈ {-2, -1, 0, 1, 2}; refine ⟨ ?_, inst✝:SetTheoryx✝:ℤ⊢ x✝ ∈ {-2, -1, 0, 1, 2} → x✝ ∈ (fun n ↦ n ^ 2) ⁻¹' {0, 1, 4} All goals completed! 🐙 ⟩; inst✝:SetTheoryx✝:ℤh✝:(fun n ↦ n ^ 2) x✝ = 0⊢ x✝ ∈ {-2, -1, 0, 1, 2}inst✝:SetTheoryx✝:ℤh✝:(fun n ↦ n ^ 2) x✝ = 1⊢ x✝ ∈ {-2, -1, 0, 1, 2}inst✝:SetTheoryx✝:ℤh:(fun n ↦ n ^ 2) x✝ ∈ {4}⊢ x✝ ∈ {-2, -1, 0, 1, 2} on_goal 3 => have : 2 ^ 2 = (4:ℤ) := (inst✝:SetTheoryx✝:ℤh:(fun n ↦ n ^ 2) x✝ ∈ {4}⊢ 2 ^ 2 = 4 All goals completed! 🐙); inst✝:SetTheoryx✝:ℤh:(fun n ↦ n ^ 2) x✝ ∈ {4}this:2 = x✝ ∨ 2 = -x✝⊢ x✝ ∈ {-2, -1, 0, 1, 2} all_goals 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 := pow@[coe] def SetTheory.Set.coe_of_fun {X Y:Set} (f: X → Y) : Object := function_to_object X Y f

This coercion has to be a CoeOut rather than a Coe because the input type X → Y contains parameters not present in the output type Object

instance SetTheory.Set.inst_coe_of_fun {X Y:Set} : CoeOut (X → Y) Object where coe := coe_of_fun
@[simp] theorem SetTheory.Set.coe_of_fun_inj {X Y:Set} (f g:X → Y) : (f:Object) = (g:Object) ↔ f = g := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypeg:X.toSubtype → Y.toSubtype⊢ ↑f = ↑g ↔ f = g All goals completed! 🐙

Axiom 3.11 (Power set axiom)

@[simp] theorem SetTheory.Set.powerset_axiom {X Y:Set} (F:Object) : F ∈ (X ^ Y) ↔ ∃ f: Y → X, f = F := SetTheory.powerset_axiom X Y F

Example 3.4.9

abbrev f_3_4_9_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_9_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_9_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_9_d : ({4,7}:Set) → ({0,1}:Set) := fun x ↦ ⟨ 1, inst✝:SetTheoryx:{4, 7}.toSubtype⊢ 1 ∈ {0, 1} All goals completed! 🐙 ⟩theorem SetTheory.Set.example_3_4_9 (F:Object) : F ∈ ({0,1}:Set) ^ ({4,7}:Set) ↔ F = f_3_4_9_a ∨ F = f_3_4_9_b ∨ F = f_3_4_9_c ∨ F = f_3_4_9_d := inst✝:SetTheoryF:Object⊢ F ∈ {0, 1} ^ {4, 7} ↔ F = ↑f_3_4_9_a ∨ F = ↑f_3_4_9_b ∨ F = ↑f_3_4_9_c ∨ F = ↑f_3_4_9_d inst✝:SetTheoryF:Object⊢ (∃ f, ↑f = F) ↔ F = ↑f_3_4_9_a ∨ F = ↑f_3_4_9_b ∨ F = ↑f_3_4_9_c ∨ F = ↑f_3_4_9_d refine ⟨?_, inst✝:SetTheoryF:Object⊢ F = ↑f_3_4_9_a ∨ F = ↑f_3_4_9_b ∨ F = ↑f_3_4_9_c ∨ F = ↑f_3_4_9_d → ∃ f, ↑f = F All goals completed! 🐙 ⟩ inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtype⊢ ↑f = ↑f_3_4_9_a ∨ ↑f = ↑f_3_4_9_b ∨ ↑f = ↑f_3_4_9_c ∨ ↑f = ↑f_3_4_9_d have h1 := (f ⟨4, inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtype⊢ 4 ∈ {4, 7} All goals completed! 🐙⟩).property have h2 := (f ⟨7, inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh1:↑(f ⟨4, ⋯⟩) ∈ {0, 1}⊢ 7 ∈ {4, 7} All goals completed! 🐙⟩).property inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh1:↑(f ⟨4, ⋯⟩) = 0 ∨ ↑(f ⟨4, ⋯⟩) = 1h2:↑(f ⟨7, ⋯⟩) = 0 ∨ ↑(f ⟨7, ⋯⟩) = 1⊢ f = f_3_4_9_a ∨ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_d inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh2:↑(f ⟨7, ⋯⟩) = 0 ∨ ↑(f ⟨7, ⋯⟩) = 1h✝:↑(f ⟨4, ⋯⟩) = 0⊢ f = f_3_4_9_a ∨ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_dinst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh2:↑(f ⟨7, ⋯⟩) = 0 ∨ ↑(f ⟨7, ⋯⟩) = 1h✝:↑(f ⟨4, ⋯⟩) = 1⊢ f = f_3_4_9_a ∨ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_d inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh2:↑(f ⟨7, ⋯⟩) = 0 ∨ ↑(f ⟨7, ⋯⟩) = 1h✝:↑(f ⟨4, ⋯⟩) = 0⊢ f = f_3_4_9_a ∨ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_dinst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh2:↑(f ⟨7, ⋯⟩) = 0 ∨ ↑(f ⟨7, ⋯⟩) = 1h✝:↑(f ⟨4, ⋯⟩) = 1⊢ f = f_3_4_9_a ∨ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_d inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 0⊢ f = f_3_4_9_a ∨ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_dinst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 1⊢ f = f_3_4_9_a ∨ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_d map_tacs [inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 0h✝:↑(f ⟨7, ⋯⟩) = 0⊢ f = f_3_4_9_a; (inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 0h✝:↑(f ⟨7, ⋯⟩) = 1⊢ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_d;inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 0h✝:↑(f ⟨7, ⋯⟩) = 1⊢ f = f_3_4_9_b); (inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 0⊢ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_d;inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 0⊢ f = f_3_4_9_c ∨ f = f_3_4_9_d;inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 0⊢ f = f_3_4_9_c); (inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 1⊢ f = f_3_4_9_b ∨ f = f_3_4_9_c ∨ f = f_3_4_9_d;inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 1⊢ f = f_3_4_9_c ∨ f = f_3_4_9_d;inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 1⊢ f = f_3_4_9_d)] all_goals inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 1val✝:Objecthx:val✝ ∈ {4, 7}⊢ ↑(f ⟨val✝, hx⟩) = ↑(f_3_4_9_d ⟨val✝, hx⟩); inst✝:SetTheoryf:{4, 7}.toSubtype → {0, 1}.toSubtypeh✝¹:↑(f ⟨4, ⋯⟩) = 1h✝:↑(f ⟨7, ⋯⟩) = 1val✝:Objecthx✝:val✝ ∈ {4, 7}hx:val✝ = 4 ∨ val✝ = 7⊢ ↑(f ⟨val✝, hx⟩) = ↑(f_3_4_9_d ⟨val✝, hx⟩); All goals completed! 🐙

Exercise 3.4.6 (i). One needs to provide a suitable definition of the power set here.

def declaration uses `sorry`SetTheory.Set.powerset (X:Set) : Set := (({0,1} ^ X): Set).replace (P := sorry) (inst✝:SetTheoryX:Set⊢ ∀ (x : ({0, 1} ^ X).toSubtype) (y y' : Object), sorry x y ∧ sorry x y' → y = y' All goals completed! 🐙)

Exercise 3.4.6 (i)

open Classical in@[simp] 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! 🐙

Lemma 3.4.10

theorem SetTheory.Set.exists_powerset (X:Set) : ∃ (Z: Set), ∀ x, x ∈ Z ↔ ∃ Y:Set, x = Y ∧ Y ⊆ X := inst✝:SetTheoryX:Set⊢ ∃ Z, ∀ (x : Object), x ∈ Z ↔ ∃ Y, x = set_to_object Y ∧ Y ⊆ X inst✝:SetTheoryX:Set⊢ ∀ (x : Object), x ∈ X.powerset ↔ ∃ Y, x = set_to_object Y ∧ Y ⊆ X; All goals completed! 🐙

Remark 3.4.11

/- As noted in errata, Exercise 3.4.6 (ii) is replaced by Exercise 3.5.11. -/ theorem 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} inst✝:SetTheorya:Objectb:Objectc:Objectx:Object⊢ (∃ Y, x = set_to_object Y ∧ ∀ x ∈ Y, x = a ∨ x = b ∨ x = c) ↔ 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} refine ⟨ ?_, inst✝:SetTheorya:Objectb:Objectc:Objectx:Object⊢ 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} → ∃ Y, x = set_to_object Y ∧ ∀ x ∈ Y, x = a ∨ x = b ∨ x = c All goals completed! 🐙 ⟩ inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = c⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝:a ∈ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝:a ∉ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c} inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝:a ∈ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝:a ∉ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c} inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝¹:a ∉ Yh✝:b ∈ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝¹:a ∉ Yh✝:b ∉ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c} inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝¹:a ∈ Yh✝:b ∈ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝¹:a ∈ Yh✝:b ∉ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝¹:a ∉ Yh✝:b ∈ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝¹:a ∉ Yh✝:b ∉ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c} inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object ∅ ∨ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c} on_goal 8 => inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object ∅ on_goal 4 => inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∉ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∉ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {a} on_goal 6 => inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {b} on_goal 7 => inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {c} on_goal 2 => inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∉ Y⊢ set_to_object Y = set_to_object {a, b} on_goal 3 => inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∉ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a, c} on_goal 5 => inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {b, c} on_goal 1 => inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a} ∨ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {b} ∨ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {c} ∨ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a, b} ∨ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a, c} ∨ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {b, c} ∨ set_to_object Y = set_to_object {a, b, c}; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∈ Yh✝¹:b ∈ Yh✝:c ∈ Y⊢ set_to_object Y = set_to_object {a, b, c} all_goals inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∉ Y⊢ Y = ∅; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∉ Yx✝:Object⊢ x✝ ∈ Y ↔ x✝ ∈ ∅; inst✝:SetTheorya:Objectb:Objectc:ObjectY:SethY:∀ x ∈ Y, x = a ∨ x = b ∨ x = ch✝²:a ∉ Yh✝¹:b ∉ Yh✝:c ∉ Yx✝:Object⊢ x✝ ∉ Y; All goals completed! 🐙

Axiom 3.12 (Union)

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

Example 3.4.12

theorem declaration uses `sorry`SetTheory.Set.example_3_4_12 : 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! 🐙

Connection with Mathlib union

theorem 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} inst✝:SetTheoryA:Setx✝:Object⊢ x✝ ∈ {x | x ∈ union A} ↔ x✝ ∈ ⋃₀ {S | ∃ S', S = {x | x ∈ S'} ∧ set_to_object S' ∈ A}; inst✝:SetTheoryA:Setx✝:Object⊢ (∃ S, x✝ ∈ S ∧ set_to_object S ∈ A) ↔ ∃ S', set_to_object S' ∈ A ∧ x✝ ∈ S'; All goals completed! 🐙

Indexed union

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' intro _ inst✝:SetTheoryI:SetA:I.toSubtype → Setx✝:I.toSubtypey✝:Object⊢ ∀ (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'✝: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✝ y✝h2:(fun α S ↦ S = set_to_object (A α)) x✝ y'✝⊢ 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 α All goals completed! 🐙 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 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} inst✝:SetTheory⊢ ∀ (x : Object), x ∈ {1, 2, 3}.iUnion index_example ↔ x ∈ {2, 3, 4, 5}; inst✝:SetTheoryx✝:Object⊢ x✝ ∈ {1, 2, 3}.iUnion index_example ↔ x✝ ∈ {2, 3, 4, 5}; inst✝:SetTheoryx✝:Object⊢ (∃ a, ∃ (h : a = 1 ∨ a = 2 ∨ a = 3), x✝ ∈ if a = 1 then {2} ∪ {3} else if a = 2 then {3} ∪ {4} else {4} ∪ {5}) ↔ x✝ = 2 ∨ x✝ = 3 ∨ x✝ = 4 ∨ x✝ = 5 refine ⟨ inst✝:SetTheoryx✝:Object⊢ (∃ a, ∃ (h : a = 1 ∨ a = 2 ∨ a = 3), x✝ ∈ if a = 1 then {2} ∪ {3} else if a = 2 then {3} ∪ {4} else {4} ∪ {5}) → x✝ = 2 ∨ x✝ = 3 ∨ x✝ = 4 ∨ x✝ = 5 All goals completed! 🐙, ?_ ⟩; inst✝:SetTheoryx✝:Objecth✝:x✝ = 2⊢ ∃ a, ∃ (h : a = 1 ∨ a = 2 ∨ a = 3), x✝ ∈ if a = 1 then {2} ∪ {3} else if a = 2 then {3} ∪ {4} else {4} ∪ {5}inst✝:SetTheoryx✝:Objecth✝:x✝ = 3⊢ ∃ a, ∃ (h : a = 1 ∨ a = 2 ∨ a = 3), x✝ ∈ if a = 1 then {2} ∪ {3} else if a = 2 then {3} ∪ {4} else {4} ∪ {5}inst✝:SetTheoryx✝:Objecth✝:x✝ = 4 ∨ x✝ = 5⊢ ∃ a, ∃ (h : a = 1 ∨ a = 2 ∨ a = 3), x✝ ∈ if a = 1 then {2} ∪ {3} else if a = 2 then {3} ∪ {4} else {4} ∪ {5}; map_tacs [inst✝:SetTheoryx✝:Objecth✝:x✝ = 2⊢ ∃ (h : 1 = 1 ∨ 1 = 2 ∨ 1 = 3), x✝ ∈ if 1 = 1 then {2} ∪ {3} else if 1 = 2 then {3} ∪ {4} else {4} ∪ {5}; inst✝:SetTheoryx✝:Objecth✝:x✝ = 3⊢ ∃ (h : 2 = 1 ∨ 2 = 2 ∨ 2 = 3), x✝ ∈ if 2 = 1 then {2} ∪ {3} else if 2 = 2 then {3} ∪ {4} else {4} ∪ {5}; inst✝:SetTheoryx✝:Objecth✝:x✝ = 4 ∨ x✝ = 5⊢ ∃ (h : 3 = 1 ∨ 3 = 2 ∨ 3 = 3), x✝ ∈ if 3 = 1 then {2} ∪ {3} else if 3 = 2 then {3} ∪ {4} else {4} ∪ {5}] all_goals All goals completed! 🐙

Connection with Mathlib indexed union

theorem 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 α} inst✝:SetTheoryI:SetA:I.toSubtype → Setx✝:Object⊢ x✝ ∈ {x | x ∈ I.iUnion A} ↔ x✝ ∈ ⋃ α, {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! 🐙

Indexed intersection

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

Exercise 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! 🐙

Exercise 3.4.3.

/- Exercise 3.4.2. State and prove an assertion connecting `preimage f (image f S)` and `S`. -/ -- theorem SetTheory.Set.preimage_of_image {X Y:Set} (f:X → Y) (S: Set) (hS: S ⊆ X) : sorry := by sorry /- Exercise 3.4.2. State and prove an assertion connecting `image f (preimage f U)` and `U`. Interestingly, it is not needed for U to be a subset of Y. -/ -- theorem SetTheory.Set.image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry /- Exercise 3.4.2. State and prove an assertion connecting `preimage f (image f (preimage f U))` and `preimage f U`. Interestingly, it is not needed for U to be a subset of Y. -/ -- theorem SetTheory.Set.preimage_of_image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry 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! 🐙def declaration uses `sorry`SetTheory.Set.image_of_inter' : Decidable (∀ X Y:Set, ∀ f:X → Y, ∀ A B: Set, image f (A ∩ B) = (image f A) ∩ (image f B)) := inst✝:SetTheory⊢ Decidable (∀ (X Y : Set) (f : X.toSubtype → Y.toSubtype) (A B : Set), image f (A ∩ B) = image f A ∩ image f B) -- The first line of this construction should be either `apply isTrue` or `apply isFalse` All goals completed! 🐙def declaration uses `sorry`SetTheory.Set.image_of_diff' : Decidable (∀ X Y:Set, ∀ f:X → Y, ∀ A B: Set, image f (A \ B) = (image f A) \ (image f B)) := inst✝:SetTheory⊢ Decidable (∀ (X Y : Set) (f : X.toSubtype → Y.toSubtype) (A B : Set), image f (A \ B) = image f A \ image f B) -- The first line of this construction should be either `apply isTrue` or `apply isFalse` All goals completed! 🐙

Exercise 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! 🐙

Exercise 3.4.5 (image of a preimage)

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

Exercise 3.4.5 (preimage of an image)

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

Helper lemma for Exercise 3.4.7.

@[simp] lemma SetTheory.Set.mem_powerset' {S S' : Set} : (S': Object) ∈ S.powerset ↔ S' ⊆ S := inst✝:SetTheoryS:SetS':Set⊢ set_to_object S' ∈ S.powerset ↔ S' ⊆ S All goals completed! 🐙

Another helper lemma for Exercise 3.4.7.

lemma SetTheory.Set.mem_union_powerset_replace_iff {S : Set} {P : S.powerset → Object → Prop} {hP : _} {x : Object} : x ∈ union (S.powerset.replace (P := P) hP) ↔ ∃ (S' : S.powerset) (U : Set), P S' U ∧ x ∈ U := inst✝:SetTheoryS:SetP:S.powerset.toSubtype → Object → ProphP:∀ (x : S.powerset.toSubtype) (y y' : Object), P x y ∧ P x y' → y = y'x:Object⊢ x ∈ union (S.powerset.replace hP) ↔ ∃ S' U, P S' (set_to_object U) ∧ x ∈ U All goals completed! 🐙

Exercise 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 = f := inst✝:SetTheoryX:SetY:Set⊢ ∃ Z, ∀ (F : Object), F ∈ Z ↔ ∃ X' Y', X' ⊆ X ∧ Y' ⊆ Y ∧ ∃ f, F = ↑f All goals completed! 🐙

Exercise 3.4.8. The point of this exercise is to prove it without using the pairwise union operation ∪.

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

Exercise 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! 🐙

Exercise 3.4.10 (union over a union of index sets)

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

Exercise 3.4.10 (a union of nonempty index sets is nonempty)

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

Exercise 3.4.10 (intersection over a union of index sets)

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

Exercise 3.4.11 (complement of a union)

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

Exercise 3.4.11 (complement of an intersection)

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