Analysis I, Section 3.5: Cartesian products

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:

• Ordered pairs and n-tuples.
• Cartesian products and n-fold products.
• Finite choice.
• Connections with Mathlib counterparts such as Set.pi and Set.prod.

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)

structure Chapter3.OrderedPair [SetTheory] : Type u_2

Definition 3.5.1 (Ordered pair). One could also have used Object × Object to define OrderedPair here.

• fst : Object
• snd : Object

theorem Chapter3.OrderedPair.ext_iff {inst✝ : SetTheory} {x y : OrderedPair} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

theorem Chapter3.OrderedPair.ext {inst✝ : SetTheory} {x y : OrderedPair} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y

@[simp]

theorem Chapter3.OrderedPair.eq [SetTheory] (x y x' y' : Object) : { fst := x, snd := y } = { fst := x', snd := y' } ↔ x = x' ∧ y = y'

Definition 3.5.1 (Ordered pair)

theorem Chapter3.SetTheory.Set.pair_eq_singleton_iff [SetTheory] {a b c : Object} : {a, b} = {c} ↔ a = c ∧ b = c

Helper lemma for Exercise 3.5.1

def Chapter3.OrderedPair.toObject [SetTheory] : OrderedPair ↪ Object

Exercise 3.5.1, first part

Equations

• One or more equations did not get rendered due to their size.

instance Chapter3.OrderedPair.inst_coeObject [SetTheory] : Coe OrderedPair Object

Equations

• Chapter3.OrderedPair.inst_coeObject = { coe := ⇑Chapter3.OrderedPair.toObject }

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.slice [SetTheory] (x : Object) (Y : Set) : Set

A technical operation, turning a object x and a set Y to a set {x} × Y, needed to define the full Cartesian product

Equations

• Chapter3.SetTheory.Set.slice x Y = Y.replace ⋯

@[simp]

theorem Chapter3.SetTheory.Set.mem_slice [SetTheory] (x z : Object) (Y : Set) : z ∈ slice x Y ↔ ∃ (y : Y.toSubtype), z = OrderedPair.toObject { fst := x, snd := ↑y }

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.cartesian [SetTheory] (X Y : Set) : Set

Definition 3.5.4 (Cartesian product)

Equations

• X.cartesian Y = Chapter3.SetTheory.union (X.replace ⋯)

instance Chapter3.SetTheory.Set.inst_SProd [SetTheory] : SProd Set Set Set

This instance enables the ×ˢ notation for Cartesian product.

Equations

• Chapter3.SetTheory.Set.inst_SProd = { sprod := Chapter3.SetTheory.Set.cartesian }

@[simp]

theorem Chapter3.SetTheory.Set.mem_cartesian [SetTheory] (z : Object) (X Y : Set) : z ∈ X ×ˢ Y ↔ ∃ (x : X.toSubtype) (y : Y.toSubtype), z = OrderedPair.toObject { fst := ↑x, snd := ↑y }

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.fst [SetTheory] {X Y : Set} (z : (X ×ˢ Y).toSubtype) : X.toSubtype

Equations

• Chapter3.SetTheory.Set.fst z = ⋯.choose

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.snd [SetTheory] {X Y : Set} (z : (X ×ˢ Y).toSubtype) : Y.toSubtype

Equations

• Chapter3.SetTheory.Set.snd z = ⋯.choose

theorem Chapter3.SetTheory.Set.pair_eq_fst_snd [SetTheory] {X Y : Set} (z : (X ×ˢ Y).toSubtype) : ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }

def Chapter3.SetTheory.Set.mk_cartesian [SetTheory] {X Y : Set} (x : X.toSubtype) (y : Y.toSubtype) : (X ×ˢ Y).toSubtype

This equips an OrderedPair with proofs that x ∈ X and y ∈ Y.

Equations

• Chapter3.SetTheory.Set.mk_cartesian x y = ⟨Chapter3.OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩

@[simp]

theorem Chapter3.SetTheory.Set.fst_of_mk_cartesian [SetTheory] {X Y : Set} (x : X.toSubtype) (y : Y.toSubtype) : fst (mk_cartesian x y) = x

@[simp]

theorem Chapter3.SetTheory.Set.snd_of_mk_cartesian [SetTheory] {X Y : Set} (x : X.toSubtype) (y : Y.toSubtype) : snd (mk_cartesian x y) = y

@[simp]

theorem Chapter3.SetTheory.Set.mk_cartesian_fst_snd_eq [SetTheory] {X Y : Set} (z : (X ×ˢ Y).toSubtype) : mk_cartesian (fst z) (snd z) = z

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.prod_equiv_prod [SetTheory] (X Y : Set) : ↑{x : Object | x ∈ X ×ˢ Y} ≃ ↑({x : Object | x ∈ X} ×ˢ {x : Object | x ∈ Y})

Connections with the Mathlib set product, which consists of Lean pairs like (x, y) equipped with a proof that x is in the left set, and y is in the right set. Lean pairs like (x, y) are similar to our OrderedPair, but more general.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Example 3.5.5 / Exercise 3.6.5. There is a bijection between X ×ˢ Y and Y ×ˢ X.

Equations

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

@[reducible, inline]

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

Example 3.5.5. A function of two variables can be thought of as a function of a pair.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Definition 3.5.6. The indexing set I plays the role of { i : 1 ≤ i ≤ n } in the text. See Exercise 3.5.10 below for some connections betweeen this concept and the preceding notion of Cartesian product and ordered pair.

Equations

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

@[reducible, inline]

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

Definition 3.5.6

Equations

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

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

Definition 3.5.6

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

@[simp]

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

@[reducible, inline]

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

Example 3.5.8. There is a bijection between (X ×ˢ Y) ×ˢ Z and X ×ˢ (Y ×ˢ Z).

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.singleton_iProd_equiv [SetTheory] (i : Object) (X : Set) : (iProd fun (x : {i}.toSubtype) => X).toSubtype ≃ X.toSubtype

Example 3.5.10. I suspect most of the equivalences will require classical reasoning and only be defined non-computably, but would be happy to learn of counterexamples.

Equations

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

@[reducible, inline]

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

Example 3.5.10

Equations

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

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_of_const_equiv [SetTheory] (I X : Set) : (iProd fun (x : I.toSubtype) => X).toSubtype ≃ (I.toSubtype → X.toSubtype)

Example 3.5.10

Equations

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

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_equiv_prod [SetTheory] (X : {0, 1}.toSubtype → Set) : (iProd X).toSubtype ≃ (X ⟨0, ⋯⟩ ×ˢ X ⟨1, ⋯⟩).toSubtype

Example 3.5.10

Equations

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

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_equiv_prod_triple [SetTheory] (X : {0, 1, 2}.toSubtype → Set) : (iProd X).toSubtype ≃ (X ⟨0, ⋯⟩ ×ˢ X ⟨1, ⋯⟩ ×ˢ X ⟨2, ⋯⟩).toSubtype

Example 3.5.10

Equations

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

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_equiv_pi [SetTheory] (I : Set) (X : I.toSubtype → Set) : (iProd X).toSubtype ≃ ↑(Set.univ.pi fun (i : I.toSubtype) => {x : Object | x ∈ X i})

Connections with Mathlib's Set.pi

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.Fin [SetTheory] (n : ℕ) : Set

Here we set up some an analogue of Mathlib Fin n types within the Chapter 3 Set Theory, with rudimentary API.

Equations

• Chapter3.SetTheory.Set.Fin n = Chapter3.nat.specify fun (m : Chapter3.nat.toSubtype) => Chapter3.SetTheory.Set.nat_equiv.symm m < n

theorem Chapter3.SetTheory.Set.mem_Fin [SetTheory] (n : ℕ) (x : Object) : x ∈ Fin n ↔ ∃ m < n, x = ↑m

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.Fin_mk [SetTheory] (n m : ℕ) (h : m < n) : (Fin n).toSubtype

Equations

• Chapter3.SetTheory.Set.Fin_mk n m h = ⟨↑m, ⋯⟩

theorem Chapter3.SetTheory.Set.mem_Fin' [SetTheory] {n : ℕ} (x : (Fin n).toSubtype) : ∃ (m : ℕ) (h : m < n), x = Fin_mk n m h

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.Fin.toNat [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) : ℕ

Equations

• ↑i = ⋯.choose

noncomputable instance Chapter3.SetTheory.Set.Fin.inst_coeNat [SetTheory] {n : ℕ} : CoeOut (Fin n).toSubtype ℕ

Equations

• Chapter3.SetTheory.Set.Fin.inst_coeNat = { coe := Chapter3.SetTheory.Set.Fin.toNat }

theorem Chapter3.SetTheory.Set.Fin.toNat_spec [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) : ∃ (h : ↑i < n), i = Fin_mk n (↑i) h

theorem Chapter3.SetTheory.Set.Fin.toNat_lt [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) : ↑i < n

@[simp]

theorem Chapter3.SetTheory.Set.Fin.coe_toNat [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) : ↑↑i = ↑i

@[simp]

theorem Chapter3.SetTheory.Set.Fin.coe_inj [SetTheory] {n : ℕ} {i j : (Fin n).toSubtype} : i = j ↔ ↑i = ↑j

@[simp]

theorem Chapter3.SetTheory.Set.Fin.coe_eq_iff [SetTheory] {n : ℕ} (i : (Fin n).toSubtype) {j : ℕ} : ↑i = ↑j ↔ ↑i = j

@[simp]

theorem Chapter3.SetTheory.Set.Fin.coe_eq_iff' [SetTheory] {n m : ℕ} (i : (Fin n).toSubtype) (hi : ↑i ∈ Fin m) : ↑⟨↑i, hi⟩ = ↑i

@[simp]

theorem Chapter3.SetTheory.Set.Fin.toNat_mk [SetTheory] {n : ℕ} (m : ℕ) (h : m < n) : ↑(Fin_mk n m h) = m

@[reducible, inline]

abbrev Chapter3.SetTheory.Set.Fin_embed [SetTheory] (n N : ℕ) (h : n ≤ N) (i : (Fin n).toSubtype) : (Fin N).toSubtype

Equations

• Chapter3.SetTheory.Set.Fin_embed n N h i = ⟨↑i, ⋯⟩

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.Fin.Fin_equiv_Fin [SetTheory] (n : ℕ) : (Fin n).toSubtype ≃ _root_.Fin n

Connections with Mathlib's Fin n

Equations

• One or more equations did not get rendered due to their size.

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

Lemma 3.5.11 (finite choice)

@[reducible, inline]

abbrev Chapter3.OrderedPair.toObject' [SetTheory] : OrderedPair ↪ Object

Exercise 3.5.1, second part (requires axiom of regularity)

Equations

• Chapter3.OrderedPair.toObject' = { toFun := fun (p : Chapter3.OrderedPair) => Chapter3.SetTheory.set_to_object {p.fst, Chapter3.SetTheory.set_to_object {p.fst, p.snd}}, inj' := ⋯ }

structure Chapter3.SetTheory.Set.Tuple [SetTheory] (n : ℕ) : Type (max u_1 u_2)

An alternate definition of a tuple, used in Exercise 3.5.2

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

theorem Chapter3.SetTheory.Set.Tuple.ext [SetTheory] {n : ℕ} {t t' : Tuple n} (hX : t.X = t'.X) (hx : ∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1)) : t = t'

Custom extensionality lemma for Exercise 3.5.2. Placing @[ext] on the structure would generate a lemma requiring proof of t.x = t'.x, but these functions have different types when t.X ≠ t'.X. This lemma handles that part.

theorem Chapter3.SetTheory.Set.Tuple.ext_iff [SetTheory] {n : ℕ} {t t' : Tuple n} : t = t' ↔ t.X = t'.X ∧ ∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1)

theorem Chapter3.SetTheory.Set.Tuple.eq [SetTheory] {n : ℕ} (t t' : Tuple n) : t = t' ↔ ∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1)

Exercise 3.5.2

@[reducible, inline]

noncomputable abbrev Chapter3.SetTheory.Set.iProd_equiv_tuples [SetTheory] (n : ℕ) (X : (Fin n).toSubtype → Set) : (iProd X).toSubtype ≃ { t : Tuple n // ∀ (i : (Fin n).toSubtype), ↑(t.x i) ∈ X i }

Equations

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

theorem Chapter3.OrderedPair.refl [SetTheory] (p : OrderedPair) : p = p

Exercise 3.5.3. The spirit here is to avoid direct rewrites (which make all of these claims trivial), and instead use OrderedPair.eq or SetTheory.Set.tuple_inj

theorem Chapter3.OrderedPair.symm [SetTheory] (p q : OrderedPair) : p = q ↔ q = p

theorem Chapter3.OrderedPair.trans [SetTheory] {p q r : OrderedPair} (hpq : p = q) (hqr : q = r) : p = r

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

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

theorem Chapter3.SetTheory.Set.tuple_trans [SetTheory] {I : Set} {X : I.toSubtype → Set} {a b c : (i : I.toSubtype) → (X i).toSubtype} (hab : tuple a = tuple b) (hbc : tuple b = tuple c) : tuple a = tuple c

theorem Chapter3.SetTheory.Set.prod_union [SetTheory] (A B C : Set) : A ×ˢ (B ∪ C) = A ×ˢ B ∪ A ×ˢ C

Exercise 3.5.4

theorem Chapter3.SetTheory.Set.prod_inter [SetTheory] (A B C : Set) : A ×ˢ (B ∩ C) = A ×ˢ B ∩ A ×ˢ C

Exercise 3.5.4

theorem Chapter3.SetTheory.Set.prod_diff [SetTheory] (A B C : Set) : A ×ˢ (B \ C) = A ×ˢ B \ A ×ˢ C

Exercise 3.5.4

theorem Chapter3.SetTheory.Set.union_prod [SetTheory] (A B C : Set) : (A ∪ B) ×ˢ C = A ×ˢ C ∪ B ×ˢ C

Exercise 3.5.4

theorem Chapter3.SetTheory.Set.inter_prod [SetTheory] (A B C : Set) : (A ∩ B) ×ˢ C = A ×ˢ C ∩ B ×ˢ C

Exercise 3.5.4

theorem Chapter3.SetTheory.Set.diff_prod [SetTheory] (A B C : Set) : (A \ B) ×ˢ C = A ×ˢ C \ B ×ˢ C

Exercise 3.5.4

theorem Chapter3.SetTheory.Set.inter_of_prod [SetTheory] (A B C D : Set) : A ×ˢ B ∩ C ×ˢ D = (A ∩ C) ×ˢ (B ∩ D)

Exercise 3.5.5

def Chapter3.SetTheory.Set.union_of_prod [SetTheory] : Decidable (∀ (A B C D : Set), A ×ˢ B ∪ C ×ˢ D = (A ∪ C) ×ˢ (B ∪ D))

Equations

• Chapter3.SetTheory.Set.union_of_prod = sorry

def Chapter3.SetTheory.Set.diff_of_prod [SetTheory] : Decidable (∀ (A B C D : Set), A ×ˢ B \ C ×ˢ D = (A \ C) ×ˢ (B \ D))

Equations

• Chapter3.SetTheory.Set.diff_of_prod = sorry

theorem Chapter3.SetTheory.Set.prod_subset_prod [SetTheory] {A B C D : Set} (hA : A ≠ ∅) (hB : B ≠ ∅) (hC : C ≠ ∅) (hD : D ≠ ∅) : A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D

Exercise 3.5.6.

def Chapter3.SetTheory.Set.prod_subset_prod' [SetTheory] : Decidable (∀ (A B C D : Set), A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D)

Equations

• Chapter3.SetTheory.Set.prod_subset_prod' = sorry

theorem Chapter3.SetTheory.Set.direct_sum [SetTheory] {X Y Z : Set} (f : Z.toSubtype → X.toSubtype) (g : Z.toSubtype → Y.toSubtype) : ∃! h : Z.toSubtype → (X ×ˢ Y).toSubtype, fst ∘ h = f ∧ snd ∘ h = g

Exercise 3.5.7

@[simp]

theorem Chapter3.SetTheory.Set.iProd_empty_iff [SetTheory] {n : ℕ} {X : (Fin n).toSubtype → Set} : iProd X = ∅ ↔ ∃ (i : (Fin n).toSubtype), X i = ∅

Exercise 3.5.8

theorem Chapter3.SetTheory.Set.iUnion_inter_iUnion [SetTheory] {I J : Set} (A : I.toSubtype → Set) (B : J.toSubtype → Set) : I.iUnion A ∩ J.iUnion B = (I ×ˢ J).iUnion fun (p : (I ×ˢ J).toSubtype) => A (fst p) ∩ B (snd p)

Exercise 3.5.9

@[reducible, inline]

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

Equations

• Chapter3.SetTheory.Set.graph f = (X ×ˢ Y).specify fun (p : (X ×ˢ Y).toSubtype) => f (Chapter3.SetTheory.Set.fst p) = Chapter3.SetTheory.Set.snd p

theorem Chapter3.SetTheory.Set.graph_inj [SetTheory] {X Y : Set} (f f' : X.toSubtype → Y.toSubtype) : graph f = graph f' ↔ f = f'

Exercise 3.5.10

theorem Chapter3.SetTheory.Set.is_graph [SetTheory] {X Y G : Set} (hG : G ⊆ X ×ˢ Y) (hvert : ∀ (x : X.toSubtype), ∃! y : Y.toSubtype, OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ G) : ∃! f : X.toSubtype → Y.toSubtype, G = graph f

theorem Chapter3.SetTheory.Set.powerset_axiom' [SetTheory] (X Y : Set) : ∃! S : Set, ∀ (F : Object), F ∈ S ↔ ∃ (f : Y.toSubtype → X.toSubtype), ↑f = F

Exercise 3.5.11. This trivially follows from SetTheory.Set.powerset_axiom, but the exercise is to derive it from SetTheory.Set.exists_powerset instead.

theorem Chapter3.SetTheory.Set.recursion [SetTheory] (X : Set) (f : nat.toSubtype → X.toSubtype → X.toSubtype) (c : X.toSubtype) : ∃! a : nat.toSubtype → X.toSubtype, a 0 = c ∧ ∀ (n : ℕ), a ↑(n + 1) = f (↑n) (a ↑n)

Exercise 3.5.12, with errata from web site incorporated

theorem Chapter3.SetTheory.Set.nat_unique [SetTheory] (nat' : Set) (zero : nat'.toSubtype) (succ : nat'.toSubtype → nat'.toSubtype) (succ_ne : ∀ (n : nat'.toSubtype), succ n ≠ zero) (succ_of_ne : ∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ m) (ind : ∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P n) : ∃! f : nat.toSubtype → nat'.toSubtype, Function.Bijective f ∧ f 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), f n = n' ↔ f ↑(nat_equiv.symm n + 1) = succ n'

Exercise 3.5.13