Vec #
Equations
- LO.ISigma1.«term_∷_» = Lean.ParserDescr.trailingNode `LO.ISigma1.«term_∷_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∷ ") (Lean.ParserDescr.cat `term 67))
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
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
instance
LO.ISigma1.cons_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : FirstOrder.Arithmetic.HierarchySymbol)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
instance
LO.ISigma1.mkVec₁_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : FirstOrder.Arithmetic.HierarchySymbol)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
instance
LO.ISigma1.mkVec₂_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : SigmaPiDelta)
(m : ℕ)
:
N-th element of List #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LO.ISigma1.Nth.construction = { Φ := fun (x : Fin 0 → V) => LO.ISigma1.Nth.Phi, defined := ⋯, monotone := ⋯ }
Instances For
Instances For
Instances For
@[simp]
TODO: move
Equations
- LO.ISigma1.nth v i = Classical.choose! ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
theorem
LO.ISigma1.cons_induction
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : SigmaPiDelta)
{P : V → Prop}
(hP : { Γ := Γ, rank := 1 }-Predicate P)
(nil : P 0)
(cons : ∀ (x v : V), P v → P (cons x v))
(v : V)
:
P v
theorem
LO.ISigma1.cons_ISigma1.sigma1_succ_induction
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{P : V → Prop}
(hP : 𝚺₁-Predicate P)
(nil : P 0)
(cons : ∀ (x v : V), P v → P (cons x v))
(v : V)
:
P v
theorem
LO.ISigma1.cons_ISigma1.pi1_succ_induction
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{P : V → Prop}
(hP : 𝚷₁-Predicate P)
(nil : P 0)
(cons : ∀ (x v : V), P v → P (cons x v))
(v : V)
:
P v
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
instance
LO.ISigma1.nth_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : SigmaPiDelta)
(m : ℕ)
:
@[simp]
theorem
LO.ISigma1.nth_lt_of_pos
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v : V}
(hv : 0 < v)
(i : V)
:
@[simp]
Inductivly Construction of Function on List #
- nil : 𝚺₁.Semisentence (arity + 1)
- cons : 𝚺₁.Semisentence (arity + 4)
Instances For
def
LO.ISigma1.VecRec.Blueprint.blueprint
{arity : ℕ}
(β : Blueprint arity)
:
Fixpoint.Blueprint arity
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.ISigma1.VecRec.Blueprint.graphDef
{arity : ℕ}
(β : Blueprint arity)
:
𝚺₁.Semisentence (arity + 1)
Equations
Instances For
def
LO.ISigma1.VecRec.Blueprint.resultDef
{arity : ℕ}
(β : Blueprint arity)
:
𝚺₁.Semisentence (arity + 2)
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
LO.ISigma1.VecRec.Construction
(V : Type u_1)
[ORingStruc V]
{arity : ℕ}
(β : Blueprint arity)
:
Type u_1
- nil (param : Fin arity → V) : V
- nil_defined : FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction self.nil β.nil
Instances For
def
LO.ISigma1.VecRec.Construction.Phi
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(param : Fin arity → V)
(C : Set V)
(pr : V)
:
Equations
Instances For
def
LO.ISigma1.VecRec.Construction.construction
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
:
Equations
- c.construction = { Φ := c.Phi, defined := ⋯, monotone := ⋯ }
Instances For
instance
LO.ISigma1.VecRec.Construction.instFiniteConstruction
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
:
def
LO.ISigma1.VecRec.Construction.Graph
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(param : Fin arity → V)
:
V → Prop
Equations
- c.Graph param = c.construction.Fixpoint param
Instances For
theorem
LO.ISigma1.VecRec.Construction.graph_defined
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
:
instance
LO.ISigma1.VecRec.Construction.graph_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(param : Fin arity → V)
:
instance
LO.ISigma1.VecRec.Construction.graph_definable''
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(param : Fin arity → V)
:
theorem
LO.ISigma1.VecRec.Construction.graph_case
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
{param : Fin arity → V}
{pr : V}
:
theorem
LO.ISigma1.VecRec.Construction.graph_exists
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(param : Fin arity → V)
(xs : V)
:
noncomputable def
LO.ISigma1.VecRec.Construction.result
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(param : Fin arity → V)
(xs : V)
:
V
Equations
- c.result param xs = Classical.choose! ⋯
Instances For
theorem
LO.ISigma1.VecRec.Construction.result_graph
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(param : Fin arity → V)
(xs : V)
:
@[simp]
theorem
LO.ISigma1.VecRec.Construction.result_nil
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(param : Fin arity → V)
:
@[simp]
theorem
LO.ISigma1.VecRec.Construction.result_cons
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(param : Fin arity → V)
(x xs : V)
:
theorem
LO.ISigma1.VecRec.Construction.result_defined
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
:
instance
LO.ISigma1.VecRec.Construction.result_definable
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
:
instance
LO.ISigma1.VecRec.Construction.result_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{arity : ℕ}
{β : Blueprint arity}
(c : Construction V β)
(Γ : SigmaPiDelta)
(m : ℕ)
:
Length of List #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Instances For
@[simp]
instance
LO.ISigma1.len_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : SigmaPiDelta)
(m : ℕ)
:
@[simp]
theorem
LO.ISigma1.nth_lt_len
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v i : V}
(hl : len v ≤ i)
:
@[simp]
theorem
LO.ISigma1.nth_lt_self
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{v i : V}
(hi : i < len v)
:
Maximum of List #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
@[simp]
Instances For
@[simp]
instance
LO.ISigma1.listMax_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : SigmaPiDelta)
(m : ℕ)
:
Take Last k-Element #
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
Instances For
@[simp]
Instances For
@[simp]
instance
LO.ISigma1.takeLast_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : SigmaPiDelta)
(m : ℕ)
:
@[simp]
@[simp]
Concatation #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
@[simp]
Instances For
@[simp]
instance
LO.ISigma1.concat_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : SigmaPiDelta)
(m : ℕ)
:
@[simp]
Membership #
Equations
- LO.ISigma1.MemVec x v = ∃ i < LO.ISigma1.len v, x = LO.ISigma1.nth v i
Instances For
Equations
- LO.ISigma1.«term_∈ᵥ_» = Lean.ParserDescr.trailingNode `LO.ISigma1.«term_∈ᵥ_» 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ᵥ ") (Lean.ParserDescr.cat `term 41))
Instances For
@[simp]
theorem
LO.ISigma1.nth_mem_memVec
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{i v : V}
(h : i < len v)
:
@[simp]
theorem
LO.ISigma1.le_of_memVec
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{x v : V}
(h : MemVec x v)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
instance
LO.ISigma1.memVec_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : SigmaPiDelta)
(m : ℕ)
:
Subset #
Equations
- LO.ISigma1.SubsetVec v w = ∀ (x : V), LO.ISigma1.MemVec x v → LO.ISigma1.MemVec x w
Instances For
Equations
- LO.ISigma1.«term_⊆ᵥ_» = Lean.ParserDescr.trailingNode `LO.ISigma1.«term_⊆ᵥ_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ᵥ ") (Lean.ParserDescr.cat `term 31))
Instances For
@[simp]
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
instance
LO.ISigma1.subsetVec_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : SigmaPiDelta)
(m : ℕ)
:
Repeat #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
instance
LO.ISigma1.repeatVec_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{m : ℕ}
(Γ : SigmaPiDelta)
:
@[simp]
@[simp]
theorem
LO.ISigma1.nth_repeatVec
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x k : V)
{i : V}
(h : i < k)
:
Convert to Set #
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
@[simp]
Instances For
@[simp]
instance
LO.ISigma1.vecToSet_definable'
{V : Type u_1}
[ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{m : ℕ}
(Γ : SigmaPiDelta)
: