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)

@[reducible, inline]

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

Definition 3.4.1. Interestingly, the definition does not require S to be a subset of 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

Definition 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

Alternate definition of image using axiom of specification

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})

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

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

@[reducible, inline]

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

Example 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

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

Equations

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

@[simp]

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.mem_preimage' [SetTheory] {X Y : Set} (f : X.toSubtype → Y.toSubtype) (U : Set) (x : Object) : x ∈ preimage f U ↔ ∃ (x' : X.toSubtype), ↑x' = x ∧ ↑(f x') ∈ U

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

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})

Connection with Mathlib's notion of preimage.

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

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

Example 3.4.6

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 }

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

Equations

• ↑f = (Chapter3.SetTheory.function_to_object X Y) f

instance Chapter3.SetTheory.Set.inst_coe_of_fun [SetTheory] {X Y : Set} : CoeOut (X.toSubtype → Y.toSubtype) Object

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 Output

Equations

• Chapter3.SetTheory.Set.inst_coe_of_fun = { coe := Chapter3.SetTheory.Set.coe_of_fun }

@[simp]

theorem Chapter3.SetTheory.Set.coe_of_fun_inj [SetTheory] {X Y : Set} (f g : X.toSubtype → Y.toSubtype) : ↑f = ↑g ↔ f = g

@[simp]

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

Axiom 3.11 (Power set axiom) -

@[reducible, inline]

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

Example 3.4.9

Equations

• Chapter3.f_3_4_9_a x = ⟨0, ⋯⟩

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• Chapter3.f_3_4_9_d x = ⟨1, ⋯⟩

theorem Chapter3.SetTheory.Set.example_3_4_9 [SetTheory] (F : 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

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

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

Equations

• X.powerset = ({0, 1} ^ X).replace ⋯

@[simp]

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

Exercise 3.4.6 (i)

theorem Chapter3.SetTheory.Set.exists_powerset [SetTheory] (X : Set) : ∃ (Z : Set), ∀ (x : Object), x ∈ Z ↔ ∃ (Y : Set), x = set_to_object Y ∧ Y ⊆ X

Lemma 3.4.10

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}

Remark 3.4.11

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

Axiom 3.12 (Union)

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

Example 3.4.12

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}

Connection with Mathlib union

@[reducible, inline]

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

Indexed union

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 α}

Connection with Mathlib indexed union

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

Indexed intersection

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

Exercise 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

Exercise 3.4.3.

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

def Chapter3.SetTheory.Set.image_of_inter' [SetTheory] : Decidable (∀ (X Y : Set) (f : X.toSubtype → Y.toSubtype) (A B : Set), image f (A ∩ B) = image f A ∩ image f B)

Equations

• Chapter3.SetTheory.Set.image_of_inter' = sorry

def Chapter3.SetTheory.Set.image_of_diff' [SetTheory] : Decidable (∀ (X Y : Set) (f : X.toSubtype → Y.toSubtype) (A B : Set), image f (A \ B) = image f A \ image f B)

Equations

• Chapter3.SetTheory.Set.image_of_diff' = sorry

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

Exercise 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

Exercise 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

Exercise 3.4.5

@[simp]

theorem Chapter3.SetTheory.Set.mem_powerset' [SetTheory] {S S' : Set} : set_to_object S' ∈ S.powerset ↔ S' ⊆ S

Helper lemma for Exercise 3.4.7.

theorem Chapter3.SetTheory.Set.mem_union_powerset_replace_iff [SetTheory] {S : Set} {P : S.powerset.toSubtype → Object → Prop} {hP : ∀ (x : S.powerset.toSubtype) (y y' : Object), P x y ∧ P x y' → y = y'} {x : Object} : x ∈ union (S.powerset.replace hP) ↔ ∃ (S' : S.powerset.toSubtype) (U : Set), P S' (set_to_object U) ∧ x ∈ U

Another helper lemma for Exercise 3.4.7.

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 = ↑f

Exercise 3.4.7

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

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

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

Exercise 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

Exercise 3.4.10

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

Exercise 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

Exercise 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 α

Exercise 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 α

Exercise 3.4.11