theorem
LO.Arith.open_induction
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐏𝐀⁻]
[V ⊧ₘ* 𝐈open]
{P : V → Prop}
(hP : ∃ (p : LO.FirstOrder.Semiformula ℒₒᵣ V 1), p.Open ∧ ∀ (x : V), P x ↔ (LO.FirstOrder.Semiformula.Evalm V ![x] id) p)
(zero : P 0)
(succ : ∀ (x : V), P x → P (x + 1))
(x : V)
:
P x
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LO.Arith.«term√_» = Lean.ParserDescr.node `LO.Arith.term√_ 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "√") (Lean.ParserDescr.cat `term 75))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
!⟪x, y, z, ...⟫
notation for Seq
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.pair_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐏𝐀⁻]
:
𝚺₀-Function₂ fun (a b : V) => ⟪a, b⟫ via LO.FirstOrder.Arith.pairDef
Equations
- LO.Arith.termπ₁_ = Lean.ParserDescr.node `LO.Arith.termπ₁_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "π₁") (Lean.ParserDescr.cat `term 80))
Instances For
Equations
- LO.Arith.termπ₂_ = Lean.ParserDescr.node `LO.Arith.termπ₂_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "π₂") (Lean.ParserDescr.cat `term 80))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.pair₅_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐏𝐀⁻]
[V ⊧ₘ* 𝐈open]
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 5 → V) => ⟪v 0, ⟪v 1, ⟪v 2, ⟪v 3, v 4⟫⟫⟫⟫)
LO.FirstOrder.Arith.pair₅Def
theorem
LO.Arith.pair₆_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐏𝐀⁻]
[V ⊧ₘ* 𝐈open]
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 6 → V) => ⟪v 0, ⟪v 1, ⟪v 2, ⟪v 3, ⟪v 4, v 5⟫⟫⟫⟫⟫)
LO.FirstOrder.Arith.pair₆Def
def
LO.Arith.npair
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐏𝐀⁻]
{n : ℕ}
(v : Fin n → V)
:
V
Equations
- LO.Arith.npair x_2 = 0
- LO.Arith.npair v = ⟪v 0, LO.Arith.npair fun (x : Fin n) => v x.succ⟫
Instances For
Equations
- One or more equations did not get rendered due to their size.
- LO.FirstOrder.Arith.unNpairDef i = i.elim0
Instances For
theorem
LO.Arith.hierarchy_polynomial_induction
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐏𝐀⁻]
[V ⊧ₘ* 𝐈open]
(Γ : LO.Polarity)
(m : ℕ)
[V ⊧ₘ* LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ m)]
{P : V → Prop}
(hP : { Γ := Γ.coe, rank := m }-Predicate P)
(zero : P 0)
(even : ∀ x > 0, P x → P (2 * x))
(odd : ∀ (x : V), P x → P (2 * x + 1))
(x : V)
:
P x