lean_problem_sheets / 2020.peano.peano_practice_questions

source

theorem exists_succ_true :

∃ (ν : ℕ → ℕ), ν = nat.succ

Note: this declaration is incomplete and uses sorry.

source

theorem exists_succ_false :

¬∃ (ν : ℕ → ℕ), ν = nat.succ

Note: this declaration is incomplete and uses sorry.

source

theorem succ_injective_true :

function.injective nat.succ

Note: this declaration is incomplete and uses sorry.

source

theorem succ_injective_false :

¬function.injective nat.succ

Note: this declaration is incomplete and uses sorry.

source

theorem succ_surjective_true :

function.surjective nat.succ

Note: this declaration is incomplete and uses sorry.

source

theorem succ_surjective_false :

¬function.surjective nat.succ

Note: this declaration is incomplete and uses sorry.

source

theorem all_functions_are_succ_true (ν : ℕ → ℕ) :

ν = nat.succ

Note: this declaration is incomplete and uses sorry.

source

theorem all_functions_are_succ_false :

¬∀ (ν : ℕ → ℕ), ν = nat.succ

Note: this declaration is incomplete and uses sorry.

source

theorem exists_unique_zero_true :

∃! (n : ℕ), n = 0

Note: this declaration is incomplete and uses sorry.

source

theorem exists_unique_zero_false :

¬∃! (n : ℕ), n = 0

Note: this declaration is incomplete and uses sorry.

source

def N :

set ℕ

Equations

N = {n : ℕ | true}

source

def Peano_Axiom_1 :

Prop

Equations

Peano_Axiom_1 = (0 ∈ N)

source

def Peano_Axiom_2 :

Prop

Equations

Peano_Axiom_2 = sorry

Note: this declaration is incomplete and uses sorry.

source

def Peano_Axiom_3 :

Prop

Equations

Peano_Axiom_3 = sorry

Note: this declaration is incomplete and uses sorry.

source

def Peano_Axiom_4 :

Prop

Equations

Peano_Axiom_4 = sorry

Note: this declaration is incomplete and uses sorry.

source

def Peano_Axiom_5 :

Prop

Equations

Peano_Axiom_5 = sorry

Note: this declaration is incomplete and uses sorry.