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.

@[implicit_reducible]

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

@[implicit_reducible]

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 between 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 (indexed product)

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 (membership in an indexed product)

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 (a). 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 (b)

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 (c)

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 (d)

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 (e)

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

@[implicit_reducible]

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 (a)

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

Exercise 3.5.4 (b)

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

Exercise 3.5.4 (c)

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

Exercise 3.5.4 (d)

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

Exercise 3.5.4 (e)

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

Exercise 3.5.4 (f)

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 (a)

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

Exercise 3.5.5 (b)

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

Exercise 3.5.5 (c)

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