Common.Set.Peano

Data types and theorems used to define Peano systems.

class Peano.System {α : Type u_1} (N : Set α) (S : α → α) (e : α) : Type

A Peano system is a triple ⟨N, S, e⟩ consisting of a set N, a function S : N → N, and a member e ∈ N such that the following three conditions are met:

1. e ∉ ran S.
2. S is one-to-one.
3. Every subset A of N containing e and closed under S is N itself.

• maps_to : Set.MapsTo S N N
• mem : e ∈ N
• zero_range : e ∉ Set.range S
• injective : Function.Injective S
• induction : ∀ (A : Set α), (A ⊆ N ∧ e ∈ A ∧ ∀ a ∈ A, S a ∈ A) → A = N

instance Peano.instSystemNatUnivSuccOfNatInstOfNatNat : Peano.System Set.univ Nat.succ 0

Equations

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

def Peano.of_nat {α : Type u_1} {N : Set α} {S : α → α} {e : α} [h : Peano.System N S e] : ℕ → α

The unique (by virtue of the Recursion Theorem for ω) function that maps the natural numbers to an arbitrary Peano system.

Equations

• Peano.of_nat 0 = e
• Peano.of_nat (Nat.succ n) = S (Peano.of_nat n)

theorem Peano.nat_maps_to : ∀ {α : Type u_1} {N : Set α} {S : α → α} {e : α} [h : Peano.System N S e], Set.MapsTo Peano.of_nat Set.univ N

The of_nat function maps all natural numbers to the set N defined in the provided Peano system.

theorem Peano.nat_isomorphism : ∀ {α : Type u_1} {N : Set α} {S : α → α} {e : α} [h : Peano.System N S e], let n2p := Peano.of_nat; Set.BijOn n2p Set.univ N ∧ (∀ (n : ℕ), n2p (Nat.succ n) = S (n2p n)) ∧ n2p 0 = e

Let ⟨N, S, e⟩ be a Peano system. Then ⟨ω, σ, 0⟩ is isomorphic to ⟨N, S, e⟩, i.e., there is a function h mapping ω one-to-one onto N in a way that preserves the successor operation

h(σ(n)) = S(h(n))

and the zero element

h(0) = e.