Arithmetization.Definability.BoundedBoldface

class LO.FirstOrder.Arith.Bounded {V : Type u_2} [LO.ORingStruc V] {k : ℕ} (f : (Fin k → V) → V) :

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

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Bounded₁ {V : Type u_2} [LO.ORingStruc V] (f : V → V) :

Prop

Equations

LO.FirstOrder.Arith.Bounded₁ f = LO.FirstOrder.Arith.Bounded fun (v : Fin 1 → V) => f (v 0)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Bounded₂ {V : Type u_2} [LO.ORingStruc V] (f : V → V → V) :

Prop

Equations

LO.FirstOrder.Arith.Bounded₂ f = LO.FirstOrder.Arith.Bounded fun (v : Fin 2 → V) => f (v 0) (v 1)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Bounded₃ {V : Type u_2} [LO.ORingStruc V] (f : V → V → V → V) :

Prop

Equations

LO.FirstOrder.Arith.Bounded₃ f = LO.FirstOrder.Arith.Bounded fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)

Instances For

source

instance LO.FirstOrder.Arith.instBounded {V : Type u_2} [LO.ORingStruc V] {k : ℕ} (f : (Fin k → V) → V) [h : LO.FirstOrder.Arith.Bounded f] :

LO.FirstOrder.Arith.Bounded f

Equations

⋯ = ⋯

source

@[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

source

@[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

source

@[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

source

@[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

source

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)

source

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

source

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)

source

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)

source

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)

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

instance LO.FirstOrder.Arith.Bounded₂.hAdd {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] :

LO.FirstOrder.Arith.Bounded₂ HAdd.hAdd

Equations

⋯ = ⋯

source

instance LO.FirstOrder.Arith.Bounded₂.hMul {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻] :

LO.FirstOrder.Arith.Bounded₂ HMul.hMul

Equations

⋯ = ⋯

source

def LO.FirstOrder.Arith.BoldfaceBoundedFunction {V : Type u_2} [LO.ORingStruc V] {k : ℕ} (f : (Fin k → V) → V) :

Prop

Equations

LO.FirstOrder.Arith.BoldfaceBoundedFunction f = (LO.FirstOrder.Arith.Bounded f ∧ 𝚺₀.BoldfaceFunction f)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.BoldfaceBoundedFunction₁ {V : Type u_2} [LO.ORingStruc V] (f : V → V) :

Prop

Equations

LO.FirstOrder.Arith.BoldfaceBoundedFunction₁ f = LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin 1 → V) => f (v 0)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ {V : Type u_2} [LO.ORingStruc V] (f : V → V → V) :

Prop

Equations

LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ f = LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin 2 → V) => f (v 0) (v 1)

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ {V : Type u_2} [LO.ORingStruc V] (f : V → V → V → V) :

Prop

Equations

LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ f = LO.FirstOrder.Arith.BoldfaceBoundedFunction fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)

Instances For

source

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) :

LO.FirstOrder.Arith.Bounded f

source

theorem LO.FirstOrder.Arith.BoldfaceBoundedFunction₁.bounded {V : Type u_2} [LO.ORingStruc V] {f : V → V} (h : LO.FirstOrder.Arith.BoldfaceBoundedFunction₁ f) :

LO.FirstOrder.Arith.Bounded₁ f

source

theorem LO.FirstOrder.Arith.BoldfaceBoundedFunction₂.bounded {V : Type u_2} [LO.ORingStruc V] {f : V → V → V} (h : LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ f) :

LO.FirstOrder.Arith.Bounded₂ f

source

theorem LO.FirstOrder.Arith.BoldfaceBoundedFunction₃.bounded {V : Type u_2} [LO.ORingStruc V] {f : V → V → V → V} (h : LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ f) :

LO.FirstOrder.Arith.Bounded₃ f

source

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

source

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

source

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

source

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

source

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] :

LO.FirstOrder.Arith.BoldfaceBoundedFunction f

source

@[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] :

LO.FirstOrder.Arith.BoldfaceBoundedFunction₁ f

source

@[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] :

LO.FirstOrder.Arith.BoldfaceBoundedFunction₂ f

source

@[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] :

LO.FirstOrder.Arith.BoldfaceBoundedFunction₃ f

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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)) :

ℌ.Boldface fun (v : Fin k → V) => ∃ w ≤ fun (x : Fin l) => p x v, P v w

source

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)) :

ℌ.Boldface fun (z : Fin l → V) => P fun (x : Fin k) => f x z

source

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) :

LO.FirstOrder.Arith.BoldfaceBoundedFunction g

source

@[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

source

@[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

source

@[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

source

@[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

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)) :

ℌ.BoldfaceFunction fun (v : Fin k → V) => F fun (x : Fin l) => f x v

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

def LO.FirstOrder.Arith.attrDefinability :

Lean.ParserDescr

Equations

LO.FirstOrder.Arith.attrDefinability = Lean.ParserDescr.node `LO.FirstOrder.Arith.attrDefinability 1024 (Lean.ParserDescr.nonReservedSymbol "definability" false)

Instances For

source

def LO.FirstOrder.Arith.tacticDefinability_ :

Lean.ParserDescr

Equations

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

Instances For

source

def LO.FirstOrder.Arith.tacticDefinability?_ :

Lean.ParserDescr

Equations

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

Instances For