Analysis I, Chapter 2 epilogue

In this (technical) epilogue, we show that the "Chapter 2" natural numbers Chapter2.Nat are isomorphic in various standard senses to the standard natural numbers ℕ.

From this point onwards, Chapter2.Nat will be deprecated, and we will use the standard natural numbers ℕ instead. In particular, one should use the full Mathlib API for ℕ for all subsequent chapters, in lieu of the Chapter2.Nat API.

Filling the sorries here requires both the Chapter2.Nat API and the Mathlib API for the standard natural numbers ℕ. As such, they are excellent exercises to prepare you for the aforementioned transition.

@[reducible, inline]

abbrev Chapter2.Nat.toNat (n : Nat) : ℕ

Equations

• Chapter2.Nat.zero.toNat = 0
• n'++.toNat = n'.toNat + 1

theorem Chapter2.Nat.zero_toNat : toNat 0 = 0

theorem Chapter2.Nat.succ_toNat (n : Nat) : n++.toNat = n.toNat + 1

@[reducible, inline]

abbrev Chapter2.Nat.equivNat : Nat ≃ ℕ

Equations

• Chapter2.Nat.equivNat = { toFun := Chapter2.Nat.toNat, invFun := fun (n : ℕ) => ↑n, left_inv := Chapter2.Nat.equivNat._proof_2, right_inv := Chapter2.Nat.equivNat._proof_3 }

@[reducible, inline]

abbrev Chapter2.Nat.equivNat_order : Nat ≃o ℕ

Equations

• Chapter2.Nat.equivNat_order = { toEquiv := Chapter2.Nat.equivNat, map_rel_iff' := @Chapter2.Nat.equivNat_order._proof_4 }

@[reducible, inline]

abbrev Chapter2.Nat.equivNat_ring : Nat ≃+* ℕ

Equations

• Chapter2.Nat.equivNat_ring = { toEquiv := Chapter2.Nat.equivNat, map_mul' := Chapter2.Nat.equivNat_ring._proof_5, map_add' := Chapter2.Nat.equivNat_ring._proof_6 }

theorem Chapter2.Nat.pow_eq_pow (n m : Nat) : ↑n.toNat ^ m.toNat = n ^ m