- bounded : ∃ (t : LO.FirstOrder.Semiterm ℒₒᵣ V k), ∀ (v : Fin k → V), f v ≤ LO.FirstOrder.Semiterm.valm V v id t
Instances
theorem
LO.FirstOrder.Arith.Bounded.bounded
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{f : (Fin k → V) → V}
[self : LO.FirstOrder.Arith.Bounded f]
:
∃ (t : LO.FirstOrder.Semiterm ℒₒᵣ V k), ∀ (v : Fin k → V), f v ≤ LO.FirstOrder.Semiterm.valm V v id t
@[reducible, inline]
Equations
- LO.FirstOrder.Arith.Bounded₁ f = LO.FirstOrder.Arith.Bounded fun (v : Fin 1 → V) => f (v 0)
Instances For
@[reducible, inline]
Equations
- LO.FirstOrder.Arith.Bounded₂ f = LO.FirstOrder.Arith.Bounded fun (v : Fin 2 → V) => f (v 0) (v 1)
Instances For
@[reducible, inline]
Equations
- LO.FirstOrder.Arith.Bounded₃ f = LO.FirstOrder.Arith.Bounded fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)
Instances For
instance
LO.FirstOrder.Arith.instBounded
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
(f : (Fin k → V) → V)
[h : LO.FirstOrder.Arith.Bounded f]
:
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.FirstOrder.Arith.Bounded.var
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(i : Fin k)
:
LO.FirstOrder.Arith.Bounded fun (v : Fin k → V) => v i
@[simp]
theorem
LO.FirstOrder.Arith.Bounded.const
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(c : V)
:
LO.FirstOrder.Arith.Bounded fun (x : Fin k → V) => c
@[simp]
theorem
LO.FirstOrder.Arith.Bounded.term_retraction
{n : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(t : LO.FirstOrder.Semiterm ℒₒᵣ V n)
(e : Fin n → Fin k)
:
LO.FirstOrder.Arith.Bounded fun (v : Fin k → V) => LO.FirstOrder.Semiterm.valm V (fun (x : Fin n) => v (e x)) id t
@[simp]
theorem
LO.FirstOrder.Arith.Bounded.term
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(t : LO.FirstOrder.Semiterm ℒₒᵣ V k)
:
LO.FirstOrder.Arith.Bounded fun (v : Fin k → V) => LO.FirstOrder.Semiterm.valm V v id t
theorem
LO.FirstOrder.Arith.Bounded.retraction
{n : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.Bounded f)
(e : Fin k → Fin n)
:
LO.FirstOrder.Arith.Bounded fun (v : Fin n → V) => f fun (i : Fin k) => v (e i)
theorem
LO.FirstOrder.Arith.Bounded.comp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{l : ℕ}
{k : ℕ}
{f : (Fin l → V) → V}
{g : Fin l → (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.Bounded f)
(hg : ∀ (i : Fin l), LO.FirstOrder.Arith.Bounded (g i))
:
LO.FirstOrder.Arith.Bounded fun (v : Fin k → V) => f fun (x : Fin l) => g x v
theorem
LO.FirstOrder.Arith.Bounded₁.comp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{f : V → V}
{k : ℕ}
{g : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.Bounded₁ f)
(hg : LO.FirstOrder.Arith.Bounded g)
:
LO.FirstOrder.Arith.Bounded fun (v : Fin k → V) => f (g v)
theorem
LO.FirstOrder.Arith.Bounded₂.comp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{f : V → V → V}
{k : ℕ}
{g₁ : (Fin k → V) → V}
{g₂ : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.Bounded₂ f)
(hg₁ : LO.FirstOrder.Arith.Bounded g₁)
(hg₂ : LO.FirstOrder.Arith.Bounded g₂)
:
LO.FirstOrder.Arith.Bounded fun (v : Fin k → V) => f (g₁ v) (g₂ v)
theorem
LO.FirstOrder.Arith.Bounded₃.comp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{f : V → V → V → V}
{k : ℕ}
{g₁ : (Fin k → V) → V}
{g₂ : (Fin k → V) → V}
{g₃ : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.Bounded₃ f)
(hg₁ : LO.FirstOrder.Arith.Bounded g₁)
(hg₂ : LO.FirstOrder.Arith.Bounded g₂)
(hg₃ : LO.FirstOrder.Arith.Bounded g₃)
:
LO.FirstOrder.Arith.Bounded fun (v : Fin k → V) => f (g₁ v) (g₂ v) (g₃ v)
instance
LO.FirstOrder.Arith.Bounded₂.add
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
:
LO.FirstOrder.Arith.Bounded₂ fun (x x_1 : V) => x + x_1
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Arith.Bounded₂.mul
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
:
LO.FirstOrder.Arith.Bounded₂ fun (x x_1 : V) => x * x_1
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Arith.Bounded₂.hAdd
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
:
LO.FirstOrder.Arith.Bounded₂ HAdd.hAdd
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Arith.Bounded₂.hMul
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
:
LO.FirstOrder.Arith.Bounded₂ HMul.hMul
Equations
- ⋯ = ⋯
def
LO.FirstOrder.Arith.BoldfaceBoundedFunction
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
(f : (Fin k → V) → V)
:
Equations
- LO.FirstOrder.Arith.BoldfaceBoundedFunction f = (LO.FirstOrder.Arith.Bounded f ∧ 𝚺₀.BoldfaceFunction f)
Instances For
@[reducible, inline]
Equations
- LO.FirstOrder.Arith.BoldfaceBoundedFunction₁ f = LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin 1 → V) => f (v 0)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.BoldfaceBoundedFunction₂
{V : Type u_2}
[LO.ORingStruc V]
(f : V → V → V)
:
Equations
- LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ f = LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin 2 → V) => f (v 0) (v 1)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.BoldfaceBoundedFunction₃
{V : Type u_2}
[LO.ORingStruc V]
(f : V → V → V → V)
:
Equations
- LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ f = LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)
Instances For
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.bounded
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{f : (Fin k → V) → V}
(h : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
:
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction₁.bounded
{V : Type u_2}
[LO.ORingStruc V]
{f : V → V}
(h : LO.FirstOrder.Arith.BoldfaceBoundedFunction₁ f)
:
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction₂.bounded
{V : Type u_2}
[LO.ORingStruc V]
{f : V → V → V}
(h : LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ f)
:
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction₃.bounded
{V : Type u_2}
[LO.ORingStruc V]
{f : V → V → V → V}
(h : LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ f)
:
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.definable
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{f : (Fin k → V) → V}
(h : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
:
ℌ.BoldfaceFunction f
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction₁.definable
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{f : V → V}
(h : LO.FirstOrder.Arith.BoldfaceBoundedFunction₁ f)
:
ℌ-Function₁ f
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction₂.definable
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{f : V → V → V}
(h : LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ f)
:
ℌ-Function₂ f
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction₃.definable
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{f : V → V → V → V}
(h : LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ f)
:
ℌ-Function₃ f
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.of_polybounded_of_definable
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
(f : (Fin k → V) → V)
[hb : LO.FirstOrder.Arith.Bounded f]
[hf : 𝚺₀.BoldfaceFunction f]
:
@[simp]
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.of_polybounded_of_definable₁
{V : Type u_2}
[LO.ORingStruc V]
(f : V → V)
[hb : LO.FirstOrder.Arith.Bounded₁ f]
[hf : 𝚺₀-Function₁ f]
:
@[simp]
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.of_polybounded_of_definable₂
{V : Type u_2}
[LO.ORingStruc V]
(f : V → V → V)
[hb : LO.FirstOrder.Arith.Bounded₂ f]
[hf : 𝚺₀-Function₂ f]
:
@[simp]
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.of_polybounded_of_definable₃
{V : Type u_2}
[LO.ORingStruc V]
(f : V → V → V → V)
[hb : LO.FirstOrder.Arith.Bounded₃ f]
[hf : 𝚺₀-Function₃ f]
:
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.retraction
{n : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(e : Fin k → Fin n)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin n → V) => f fun (i : Fin k) => v (e i)
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_blt
{k : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(h : ℌ.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
ℌ.Boldface fun (v : Fin k → V) => ∀ x < f v, P v x
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_blt
{k : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(h : ℌ.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
ℌ.Boldface fun (v : Fin k → V) => ∃ x < f v, P v x
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_ble
{k : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(h : ℌ.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
ℌ.Boldface fun (v : Fin k → V) => ∀ x ≤ f v, P v x
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_ble
{k : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(h : ℌ.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
ℌ.Boldface fun (v : Fin k → V) => ∃ x ≤ f v, P v x
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_blt_zero
{k : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(h : { Γ := Γ, rank := 0 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
{ Γ := Γ, rank := 0 }.Boldface fun (v : Fin k → V) => ∀ x < f v, P v x
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_blt_zero
{k : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(h : { Γ := Γ, rank := 0 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
{ Γ := Γ, rank := 0 }.Boldface fun (v : Fin k → V) => ∃ x < f v, P v x
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_ble_zero
{k : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(h : { Γ := Γ, rank := 0 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
{ Γ := Γ, rank := 0 }.Boldface fun (v : Fin k → V) => ∀ x ≤ f v, P v x
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_ble_zero
{k : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(h : { Γ := Γ, rank := 0 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
{ Γ := Γ, rank := 0 }.Boldface fun (v : Fin k → V) => ∃ x ≤ f v, P v x
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_vec_le_boldfaceBoundedFunction
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{l : ℕ}
{k : ℕ}
{p : Fin l → (Fin k → V) → V}
{P : (Fin k → V) → (Fin l → V) → Prop}
(pp : ∀ (i : Fin l), LO.FirstOrder.Arith.BoldfaceBoundedFunction (p i))
(hP : ℌ.Boldface fun (w : Fin (k + l) → V) => P (fun (i : Fin k) => w (Fin.castAdd l i)) fun (j : Fin l) => w (Fin.natAdd k j))
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.substitution_boldfaceBoundedFunction
{k : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{P : (Fin k → V) → Prop}
{l : ℕ}
{f : Fin k → (Fin l → V) → V}
(hP : ℌ.Boldface P)
(hf : ∀ (i : Fin k), LO.FirstOrder.Arith.BoldfaceBoundedFunction (f i))
:
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.of_iff
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{f : (Fin k → V) → V}
{g : (Fin k → V) → V}
(H : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
(h : ∀ (v : Fin k → V), f v = g v)
:
@[simp]
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.var
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(i : Fin k)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin k → V) => v i
@[simp]
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.const
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(c : V)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (x : Fin k → V) => c
@[simp]
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.term_retraction
{n : ℕ}
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(t : LO.FirstOrder.Semiterm ℒₒᵣ V n)
(e : Fin n → Fin k)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin k → V) =>
LO.FirstOrder.Semiterm.valm V (fun (x : Fin n) => v (e x)) id t
@[simp]
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.term
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
(t : LO.FirstOrder.Semiterm ℒₒᵣ V k)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin k → V) => LO.FirstOrder.Semiterm.valm V v id t
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₁
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : V → Prop}
{f : (Fin k → V) → V}
[hP : ℌ-Predicate P]
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
:
ℌ.Boldface fun (v : Fin k → V) => P (f v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₂
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{R : V → V → Prop}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
[hR : ℌ-Relation R]
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
:
ℌ.Boldface fun (v : Fin k → V) => R (f₁ v) (f₂ v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₃
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{R : V → V → V → Prop}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
[hR : ℌ-Relation₃ R]
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
(hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃)
:
ℌ.Boldface fun (v : Fin k → V) => R (f₁ v) (f₂ v) (f₃ v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₄
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{R : V → V → V → V → Prop}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
{f₄ : (Fin k → V) → V}
[hR : ℌ-Relation₄ R]
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
(hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃)
(hf₄ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₄)
:
ℌ.Boldface fun (v : Fin k → V) => R (f₁ v) (f₂ v) (f₃ v) (f₄ v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₁_zero
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{P : V → Prop}
{f : (Fin k → V) → V}
[hP : { Γ := Γ, rank := 0 }-Predicate P]
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
:
{ Γ := Γ, rank := 0 }.Boldface fun (v : Fin k → V) => P (f v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₂_zero
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{R : V → V → Prop}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
[hR : { Γ := Γ, rank := 0 }-Relation R]
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
:
{ Γ := Γ, rank := 0 }.Boldface fun (v : Fin k → V) => R (f₁ v) (f₂ v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₃_zero
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{R : V → V → V → Prop}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
[hR : { Γ := Γ, rank := 0 }-Relation₃ R]
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
(hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃)
:
{ Γ := Γ, rank := 0 }.Boldface fun (v : Fin k → V) => R (f₁ v) (f₂ v) (f₃ v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bcomp₄_zero
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{R : V → V → V → V → Prop}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
{f₄ : (Fin k → V) → V}
[hR : { Γ := Γ, rank := 0 }-Relation₄ R]
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
(hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃)
(hf₄ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₄)
:
{ Γ := Γ, rank := 0 }.Boldface fun (v : Fin k → V) => R (f₁ v) (f₂ v) (f₃ v) (f₄ v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.bcomp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{l : ℕ}
{k : ℕ}
{F : (Fin l → V) → V}
{f : Fin l → (Fin k → V) → V}
(hF : ℌ.BoldfaceFunction F)
(hf : ∀ (i : Fin l), LO.FirstOrder.Arith.BoldfaceBoundedFunction (f i))
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁.bcomp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{F : V → V}
{f : (Fin k → V) → V}
(hF : ℌ-Function₁ F)
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
:
ℌ.BoldfaceFunction fun (v : Fin k → V) => F (f v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.bcomp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{F : V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
(hF : ℌ-Function₂ F)
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
:
ℌ.BoldfaceFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v)
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃.bcomp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{F : V → V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
(hF : ℌ-Function₃ F)
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
(hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃)
:
ℌ.BoldfaceFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v) (f₃ v)
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction₁.comp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{F : V → V}
{f : (Fin k → V) → V}
(hF : LO.FirstOrder.Arith.BoldfaceBoundedFunction₁ F)
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin k → V) => F (f v)
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction₂.comp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{F : V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
(hF : LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ F)
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v)
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction₃.comp
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{F : V → V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
(hF : LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ F)
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
(hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v) (f₃ v)
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.comp₁
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{F : V → V}
{f : (Fin k → V) → V}
[hFb : LO.FirstOrder.Arith.Bounded₁ F]
[hFd : 𝚺₀-Function₁ F]
(hf : LO.FirstOrder.Arith.BoldfaceBoundedFunction f)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin k → V) => F (f v)
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.comp₂
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{F : V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
[hFb : LO.FirstOrder.Arith.Bounded₂ F]
[hFd : 𝚺₀-Function₂ F]
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v)
theorem
LO.FirstOrder.Arith.BoldfaceBoundedFunction.comp₃
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{F : V → V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
[hFb : LO.FirstOrder.Arith.Bounded₃ F]
[hFd : 𝚺₀-Function₃ F]
(hf₁ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₁)
(hf₂ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₂)
(hf₃ : LO.FirstOrder.Arith.BoldfaceBoundedFunction f₃)
:
LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin k → V) => F (f₁ v) (f₂ v) (f₃ v)
Equations
- LO.FirstOrder.Arith.attrDefinability = Lean.ParserDescr.node `LO.FirstOrder.Arith.attrDefinability 1024 (Lean.ParserDescr.nonReservedSymbol "definability" false)
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.