def
LO.FirstOrder.Defined
{V : Type u_1}
{L : LO.FirstOrder.Language}
{k : ℕ}
(R : (Fin k → V) → Prop)
[LO.FirstOrder.Structure L V]
(p : LO.FirstOrder.Semisentence L k)
:
Equations
- LO.FirstOrder.Defined R p = ∀ (v : Fin k → V), R v ↔ V ⊧/v p
Instances For
def
LO.FirstOrder.DefinedWithParam
{V : Type u_1}
{L : LO.FirstOrder.Language}
{k : ℕ}
(R : (Fin k → V) → Prop)
[LO.FirstOrder.Structure L V]
(p : LO.FirstOrder.Semiformula L V k)
:
Equations
- LO.FirstOrder.DefinedWithParam R p = ∀ (v : Fin k → V), R v ↔ (LO.FirstOrder.Semiformula.Evalm V v id) p
Instances For
theorem
LO.FirstOrder.Defined.iff
{L : LO.FirstOrder.Language}
{V : Type u_2}
[LO.FirstOrder.Structure L V]
{k : ℕ}
{R : (Fin k → V) → Prop}
{p : LO.FirstOrder.Semisentence L k}
(h : LO.FirstOrder.Defined R p)
(v : Fin k → V)
:
theorem
LO.FirstOrder.DefinedWithParam.iff
{L : LO.FirstOrder.Language}
{V : Type u_2}
[LO.FirstOrder.Structure L V]
{k : ℕ}
{R : (Fin k → V) → Prop}
{p : LO.FirstOrder.Semiformula L V k}
(h : LO.FirstOrder.DefinedWithParam R p)
(v : Fin k → V)
:
(LO.FirstOrder.Semiformula.Evalm V v id) p ↔ R v
def
LO.FirstOrder.Arith.HierarchySymbol.Defined
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
(R : (Fin k → V) → Prop)
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
:
ℌ.Semisentence k → Prop
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
(R : (Fin k → V) → Prop)
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
class
LO.FirstOrder.Arith.HierarchySymbol.Lightface
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
{k : ℕ}
(P : (Fin k → V) → Prop)
:
- definable : ∃ (p : ℌ.Semisentence k), LO.FirstOrder.Arith.HierarchySymbol.Defined P p
Instances
theorem
LO.FirstOrder.Arith.HierarchySymbol.Lightface.definable
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
[self : ℌ.Lightface P]
:
∃ (p : ℌ.Semisentence k), LO.FirstOrder.Arith.HierarchySymbol.Defined P p
class
LO.FirstOrder.Arith.HierarchySymbol.Boldface
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
{k : ℕ}
(P : (Fin k → V) → Prop)
:
- definable : ∃ (p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ), LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p
Instances
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.definable
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
[self : ℌ.Boldface P]
:
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedPred
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(P : V → Prop)
(p : ℌ.Semisentence 1)
:
Equations
- (ℌ-Predicate P via p) = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 1 → V) => P (v 0)) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedRel
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(R : V → V → Prop)
(p : ℌ.Semisentence 2)
:
Equations
- (ℌ-Relation R via p) = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 2 → V) => R (v 0) (v 1)) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedRel₃
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(R : V → V → V → Prop)
(p : ℌ.Semisentence 3)
:
Equations
- (ℌ-Relation₃ R via p) = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 3 → V) => R (v 0) (v 1) (v 2)) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedRel₄
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(R : V → V → V → V → Prop)
(p : ℌ.Semisentence 4)
:
Equations
- (ℌ-Relation₄ R via p) = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 4 → V) => R (v 0) (v 1) (v 2) (v 3)) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
(f : (Fin k → V) → V)
(p : ℌ.Semisentence (k + 1))
:
Equations
- LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f p = LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succ → V) => v 0 = f fun (x : Fin k) => v x.succ) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₀
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(c : V)
(p : ℌ.Semisentence 1)
:
Equations
- (ℌ-Function₀ c via p) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (x : Fin 0 → V) => c) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₁
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V)
(p : ℌ.Semisentence 2)
:
Equations
- (ℌ-Function₁ f via p) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 1 → V) => f (v 0)) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₂
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V → V)
(p : ℌ.Semisentence 3)
:
Equations
- (ℌ-Function₂ f via p) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 2 → V) => f (v 0) (v 1)) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₃
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V → V → V)
(p : ℌ.Semisentence 4)
:
Equations
- (ℌ-Function₃ f via p) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₄
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V → V → V → V)
(p : ℌ.Semisentence 5)
:
Equations
- (ℌ-Function₄ f via p) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 4 → V) => f (v 0) (v 1) (v 2) (v 3)) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction₅
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V → V → V → V → V)
(p : ℌ.Semisentence 6)
:
Equations
- (ℌ-Function₅ f via p) = LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin 5 → V) => f (v 0) (v 1) (v 2) (v 3) (v 4)) p
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(P : V → Prop)
:
Equations
- (ℌ-Predicate P) = ℌ.Boldface fun (v : Fin 1 → V) => P (v 0)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(P : V → V → Prop)
:
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₃
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(P : V → V → V → Prop)
:
Equations
- (ℌ-Relation₃ P) = ℌ.Boldface fun (v : Fin 3 → V) => P (v 0) (v 1) (v 2)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₄
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(P : V → V → V → V → Prop)
:
Equations
- (ℌ-Relation₄ P) = ℌ.Boldface fun (v : Fin 4 → V) => P (v 0) (v 1) (v 2) (v 3)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₅
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(P : V → V → V → V → V → Prop)
:
Equations
- (ℌ-Relation₅ P) = ℌ.Boldface fun (v : Fin 5 → V) => P (v 0) (v 1) (v 2) (v 3) (v 4)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₆
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(P : V → V → V → V → V → V → Prop)
:
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
{k : ℕ}
(f : (Fin k → V) → V)
:
Equations
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₀
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(c : V)
:
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V)
:
Equations
- (ℌ-Function₁ f) = ℌ.BoldfaceFunction fun (v : Fin 1 → V) => f (v 0)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V → V)
:
Equations
- (ℌ-Function₂ f) = ℌ.BoldfaceFunction fun (v : Fin 2 → V) => f (v 0) (v 1)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V → V → V)
:
Equations
- (ℌ-Function₃ f) = ℌ.BoldfaceFunction fun (v : Fin 3 → V) => f (v 0) (v 1) (v 2)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₄
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V → V → V → V)
:
Equations
- (ℌ-Function₄ f) = ℌ.BoldfaceFunction fun (v : Fin 4 → V) => f (v 0) (v 1) (v 2) (v 3)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₅
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(f : V → V → V → V → V → V)
:
Equations
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
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
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.FirstOrder.Arith.HierarchySymbol.Defined.df
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{R : (Fin k → V) → Prop}
{p : ℌ.Semisentence k}
(h : LO.FirstOrder.Arith.HierarchySymbol.Defined R p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Defined.proper
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{R : (Fin k → V) → Prop}
{m : ℕ}
{p : { Γ := 𝚫, rank := m }.Semisentence k}
(h : LO.FirstOrder.Arith.HierarchySymbol.Defined R p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Defined.of_zero
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{R : (Fin k → V) → Prop}
{p : 𝚺₀.Semisentence k}
(h : LO.FirstOrder.Arith.HierarchySymbol.Defined R p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Defined.emb
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{R : (Fin k → V) → Prop}
{p : ℌ.Semisentence k}
(h : LO.FirstOrder.Arith.HierarchySymbol.Defined R p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Defined.of_iff
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
(h : ∀ (x : Fin k → V), P x ↔ Q x)
{p : ℌ.Semisentence k}
(H : LO.FirstOrder.Arith.HierarchySymbol.Defined Q p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
(p : ℌ.Semisentence k)
(hP : LO.FirstOrder.Arith.HierarchySymbol.Defined P p)
:
ℌ.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable₀
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{p : 𝚺₀.Semisentence k}
(hP : LO.FirstOrder.Arith.HierarchySymbol.Defined P p)
:
ℌ.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable_oRing
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
(p : ℌ.Semisentence k)
(hP : LO.FirstOrder.Arith.HierarchySymbol.Defined P p)
:
ℌ.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.Defined.to_definable_oRing₀
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
(p : 𝚺₀.Semisentence k)
(hP : LO.FirstOrder.Arith.HierarchySymbol.Defined P p)
:
ℌ.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction.of_eq
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{f : (Fin k → V) → V}
{g : (Fin k → V) → V}
(h : ∀ (x : Fin k → V), f x = g x)
{p : ℌ.Semisentence (k + 1)}
(H : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction.graph_delta
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{m : ℕ}
{f : (Fin k → V) → V}
{p : { Γ := 𝚺, rank := m }.Semisentence (k + 1)}
(h : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction f p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.df
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{R : (Fin k → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ}
(h : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R p)
:
LO.FirstOrder.DefinedWithParam R p.val
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.proper
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{R : (Fin k → V) → Prop}
{m : ℕ}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }}
(h : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.of_zero
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{R : (Fin k → V) → Prop}
{Γ' : LO.SigmaPiDelta}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := Γ', rank := 0 }}
(h : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R p)
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R (p.ofZero Γ)
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.of_deltaOne
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{R : (Fin k → V) → Prop}
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k 𝚫₁}
(h : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R (p.ofDeltaOne Γ m)
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.emb
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{R : (Fin k → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ}
(h : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam R p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.of_iff
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
(h : ∀ (x : Fin k → V), P x ↔ Q x)
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ}
(H : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam Q p)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.to_definable
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ}
(h : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
:
ℌ.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.to_definable₀
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Γ' : LO.SigmaPiDelta}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := Γ', rank := 0 }}
(h : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
:
ℌ.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.to_definable_deltaOne
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k 𝚫₁}
{Γ : LO.SigmaPiDelta}
{m : ℕ}
(h : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
:
{ Γ := Γ, rank := m + 1 }.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.retraction
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{l : ℕ}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
(f : Fin k → Fin l)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (v : Fin l → V) => P fun (i : Fin k) => v (f i))
(LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew
(LO.FirstOrder.Rew.substs fun (x : Fin k) => LO.FirstOrder.Semiterm.bvar (f x)) p)
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.verum
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (x : Fin k → V) => True) ⊤
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.falsum
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (x : Fin k → V) => False) ⊥
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.and
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ}
{q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
(hq : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam Q q)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (x : Fin k → V) => P x ∧ Q x) (p ⋏ q)
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.or
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ}
{q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k ℌ}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
(hq : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam Q q)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (x : Fin k → V) => P x ∨ Q x) (p ⋎ q)
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.negSigma
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
{m : ℕ}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := 𝚺, rank := m }}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (x : Fin k → V) => ¬P x) p.negSigma
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.negPi
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
{m : ℕ}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := 𝚷, rank := m }}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (x : Fin k → V) => ¬P x) p.negPi
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.not
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
{m : ℕ}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (x : Fin k → V) => ¬P x) (∼p)
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.imp
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
{m : ℕ}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }}
{q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
(hq : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam Q q)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (x : Fin k → V) => P x → Q x) (p ➝ q)
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.iff
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
{m : ℕ}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }}
{q : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V k { Γ := 𝚫, rank := m }}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
(hq : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam Q q)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (x : Fin k → V) => P x ↔ Q x) (p ⭤ q)
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.ball
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin (k + 1) → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V (k + 1) ℌ}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
(t : LO.FirstOrder.Semiterm ℒₒᵣ V k)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam
(fun (v : Fin k → V) => ∀ x < LO.FirstOrder.Semiterm.valm V v id t, P (x :> v))
(LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ball t p)
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.bex
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin (k + 1) → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V (k + 1) ℌ}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
(t : LO.FirstOrder.Semiterm ℒₒᵣ V k)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam
(fun (v : Fin k → V) => ∃ x < LO.FirstOrder.Semiterm.valm V v id t, P (x :> v))
(LO.FirstOrder.Arith.HierarchySymbol.Semiformula.bex t p)
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.ex
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{m : ℕ}
{P : (Fin (k + 1) → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V (k + 1) { Γ := 𝚺, rank := m + 1 }}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (v : Fin k → V) => ∃ (x : V), P (x :> v)) p.ex
theorem
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam.all
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{m : ℕ}
{P : (Fin (k + 1) → V) → Prop}
{p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula V (k + 1) { Γ := 𝚷, rank := m + 1 }}
(hp : LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam P p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedWithParam (fun (v : Fin k → V) => ∀ (x : V), P (x :> v)) p.all
@[simp]
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.eq
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
:
ℌ-Relation Eq
Equations
- ⋯ = ⋯
@[simp]
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.lt
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
:
ℌ-Relation LT.lt
Equations
- ⋯ = ⋯
@[simp]
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.le
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
:
ℌ-Relation LE.le
Equations
- ⋯ = ⋯
@[simp]
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.add
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
:
ℌ-Function₂ fun (x x_1 : V) => x + x_1
Equations
- ⋯ = ⋯
@[simp]
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.mul
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
:
ℌ-Function₂ fun (x x_1 : V) => x * x_1
Equations
- ⋯ = ⋯
@[simp]
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.hAdd
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
:
ℌ-Function₂ HAdd.hAdd
Equations
- ⋯ = ⋯
@[simp]
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.hMul
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
:
ℌ-Function₂ HMul.hMul
Equations
- ⋯ = ⋯
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.mkPolarity
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{m : ℕ}
{P : (Fin k → V) → Prop}
{Γ : LO.Polarity}
(p : LO.FirstOrder.Semiformula ℒₒᵣ V k)
(hp : LO.FirstOrder.Arith.Hierarchy Γ m p)
(hP : ∀ (v : Fin k → V), P v ↔ (LO.FirstOrder.Semiformula.Evalm V v id) p)
:
{ Γ := Γ.coe, rank := m }.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_iff
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
(H : ℌ.Boldface Q)
(h : ∀ (x : Fin k → V), P x ↔ Q x)
:
ℌ.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_oRing
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
(h : ℌ.Boldface P)
:
ℌ.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_delta
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{P : (Fin k → V) → Prop}
{m : ℕ}
(h : { Γ := 𝚫, rank := m }.Boldface P)
:
{ Γ := Γ, rank := m }.Boldface P
instance
LO.FirstOrder.Arith.HierarchySymbol.Boldface.instMkOfDeltaSigmaPiDelta
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
{m : ℕ}
[{ Γ := 𝚫, rank := m }.Boldface P]
(Γ : LO.SigmaPiDelta)
:
{ Γ := Γ, rank := m }.Boldface P
Equations
- ⋯ = ⋯
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_sigma_of_pi
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{P : (Fin k → V) → Prop}
{m : ℕ}
(hσ : { Γ := 𝚺, rank := m }.Boldface P)
(hπ : { Γ := 𝚷, rank := m }.Boldface P)
:
{ Γ := Γ, rank := m }.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_zero
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Γ' : LO.SigmaPiDelta}
(h : { Γ := Γ', rank := 0 }.Boldface P)
:
ℌ.Boldface P
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_deltaOne
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
(h : 𝚫₁.Boldface P)
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }.Boldface P
instance
LO.FirstOrder.Arith.HierarchySymbol.Boldface.instOfSigmaZero
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
[𝚺₀.Boldface P]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ.Boldface P
Equations
- ⋯ = ⋯
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.retraction
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
(h : ℌ.Boldface P)
{n : ℕ}
(f : Fin k → Fin n)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.retractiont
(n : ℕ)
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
(h : ℌ.Boldface P)
(f : Fin k → LO.FirstOrder.Semiterm ℒₒᵣ V n)
:
ℌ.Boldface fun (v : Fin n → V) => P fun (i : Fin k) => LO.FirstOrder.Semiterm.valm V v id (f i)
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.const
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : Prop}
:
ℌ.Boldface fun (x : Fin k → V) => P
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.and
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
(h₁ : ℌ.Boldface P)
(h₂ : ℌ.Boldface Q)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.conj
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{l : ℕ}
{P : Fin l → (Fin k → V) → Prop}
(h : ∀ (i : Fin l), ℌ.Boldface fun (w : Fin k → V) => P i w)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.or
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
(h₁ : ℌ.Boldface P)
(h₂ : ℌ.Boldface Q)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.not
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{P : (Fin k → V) → Prop}
{m : ℕ}
(h : { Γ := Γ.alt, rank := m }.Boldface P)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.imp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
{m : ℕ}
(h₁ : { Γ := Γ.alt, rank := m }.Boldface P)
(h₂ : { Γ := Γ, rank := m }.Boldface Q)
:
{ Γ := Γ, rank := m }.Boldface fun (v : Fin k → V) => P v → Q v
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.iff
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{P : (Fin k → V) → Prop}
{Q : (Fin k → V) → Prop}
{m : ℕ}
(h₁ : { Γ := 𝚫, rank := m }.Boldface P)
(h₂ : { Γ := 𝚫, rank := m }.Boldface Q)
{Γ : LO.SigmaPiDelta}
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.equal'
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
(i : Fin k)
(j : Fin k)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.of_sigma
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{m : ℕ}
{f : (Fin k → V) → V}
(h : { Γ := 𝚺, rank := m }.BoldfaceFunction f)
{Γ : LO.SigmaPiDelta}
:
{ Γ := Γ, rank := m }.BoldfaceFunction f
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.exVec
{V : Type u_2}
[LO.ORingStruc V]
{m : ℕ}
{k : ℕ}
{l : ℕ}
{P : (Fin k → V) → (Fin l → V) → Prop}
(h : { Γ := 𝚺, rank := m + 1 }.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.allVec
{V : Type u_2}
[LO.ORingStruc V]
{m : ℕ}
{k : ℕ}
{l : ℕ}
{P : (Fin k → V) → (Fin l → V) → Prop}
(h : { Γ := 𝚷, rank := m + 1 }.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
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{P : (Fin k → V) → Prop}
{l : ℕ}
{m : ℕ}
{f : Fin k → (Fin l → V) → V}
(hP : { Γ := Γ, rank := m + 1 }.Boldface P)
(hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction (f i))
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{P : V → Prop}
{k : ℕ}
{f : (Fin k → V) → V}
(hP : { Γ := Γ, rank := m + 1 }-Predicate P)
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{P : V → V → Prop}
{k : ℕ}
{f : (Fin k → V) → V}
{g : (Fin k → V) → V}
(hP : { Γ := Γ, rank := m + 1 }-Relation P)
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
(hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₃.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{P : V → V → V → Prop}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
(hP : { Γ := Γ, rank := m + 1 }-Relation₃ P)
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
(hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₄.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{P : 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}
(hP : { Γ := Γ, rank := m + 1 }-Relation₄ P)
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
(hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃)
(hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel₅.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{P : V → 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}
{f₅ : (Fin k → V) → V}
(hP : { Γ := Γ, rank := m + 1 }-Relation₅ P)
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
(hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃)
(hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄)
(hf₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₅)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₁
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{P : V → Prop}
{f : (Fin k → V) → V}
[{ Γ := Γ, rank := m + 1 }-Predicate P]
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₂
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{P : V → V → Prop}
{f : (Fin k → V) → V}
{g : (Fin k → V) → V}
[{ Γ := Γ, rank := m + 1 }-Relation P]
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
(hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₃
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{P : V → V → V → Prop}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
[{ Γ := Γ, rank := m + 1 }-Relation₃ P]
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
(hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₄
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{P : 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}
[{ Γ := Γ, rank := m + 1 }-Relation₄ P]
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
(hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃)
(hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₅
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{P : V → 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}
{f₅ : (Fin k → V) → V}
[{ Γ := Γ, rank := m + 1 }-Relation₅ P]
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
(hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃)
(hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄)
(hf₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₅)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfacePred.of_iff
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{P : V → Prop}
{Q : V → Prop}
(H : ℌ-Predicate Q)
(h : ∀ (x : V), P x ↔ Q x)
:
ℌ-Predicate P
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁.graph
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{f : V → V}
[h : ℌ-Function₁ f]
:
Equations
- ⋯ = h
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.graph
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{f : V → V → V}
[h : ℌ-Function₂ f]
:
Equations
- ⋯ = h
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃.graph
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{f : V → V → V → V}
[h : ℌ-Function₃ f]
:
Equations
- ⋯ = h
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.graph_delta
{V : Type u_2}
[LO.ORingStruc V]
{m : ℕ}
{k : ℕ}
{f : (Fin k → V) → V}
(h : { Γ := 𝚺, rank := m }.BoldfaceFunction f)
:
{ Γ := 𝚫, rank := m }.BoldfaceFunction f
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instMkDeltaSigmaPiDeltaOfSigma
{V : Type u_2}
[LO.ORingStruc V]
{m : ℕ}
{k : ℕ}
{f : (Fin k → V) → V}
[h : { Γ := 𝚺, rank := m }.BoldfaceFunction f]
:
{ Γ := 𝚫, rank := m }.BoldfaceFunction f
Equations
- ⋯ = ⋯
instance
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instOfSigmaZero
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
{f : (Fin k → V) → V}
[𝚺₀.BoldfaceFunction f]
:
ℌ.BoldfaceFunction f
Equations
- ⋯ = ⋯
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.of_sigmaOne
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{f : (Fin k → V) → V}
(h : 𝚺₁.BoldfaceFunction f)
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }.BoldfaceFunction f
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.var
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
(i : Fin k)
:
ℌ.BoldfaceFunction fun (v : Fin k → V) => v i
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.const
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{k : ℕ}
(c : V)
:
ℌ.BoldfaceFunction fun (x : Fin k → V) => c
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.term_retraction
(n : ℕ)
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
(t : LO.FirstOrder.Semiterm ℒₒᵣ V n)
(e : Fin n → Fin k)
:
ℌ.BoldfaceFunction fun (v : Fin k → V) => LO.FirstOrder.Semiterm.valm V (fun (x : Fin n) => v (e x)) id t
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.term
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
(t : LO.FirstOrder.Semiterm ℒₒᵣ V k)
:
ℌ.BoldfaceFunction fun (v : Fin k → V) => LO.FirstOrder.Semiterm.valm V v id t
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.of_eq
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{f : (Fin k → V) → V}
(g : (Fin k → V) → V)
(h : ∀ (v : Fin k → V), f v = g v)
(H : ℌ.BoldfaceFunction f)
:
ℌ.BoldfaceFunction g
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.retraction
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{n : ℕ}
{k : ℕ}
{f : (Fin k → V) → V}
(hf : ℌ.BoldfaceFunction f)
(e : Fin k → Fin n)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.retractiont
{V : Type u_2}
[LO.ORingStruc V]
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{n : ℕ}
{k : ℕ}
{f : (Fin k → V) → V}
(hf : ℌ.BoldfaceFunction f)
(t : Fin k → LO.FirstOrder.Semiterm ℒₒᵣ V n)
:
ℌ.BoldfaceFunction fun (v : Fin n → V) => f fun (i : Fin k) => LO.FirstOrder.Semiterm.valm V v id (t i)
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.rel
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{ℌ : LO.FirstOrder.Arith.HierarchySymbol}
{f : (Fin k → V) → V}
(h : ℌ.BoldfaceFunction f)
:
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.nth
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(i : Fin k)
:
ℌ.BoldfaceFunction fun (w : Fin k → V) => w i
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.substitution
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{k : ℕ}
{l : ℕ}
{m : ℕ}
{F : (Fin k → V) → V}
{f : Fin k → (Fin l → V) → V}
(hF : { Γ := Γ, rank := m + 1 }.BoldfaceFunction F)
(hf : ∀ (i : Fin k), { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction (f i))
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{F : V → V}
{f : (Fin k → V) → V}
(hF : { Γ := Γ, rank := m + 1 }-Function₁ F)
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{F : V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
(hF : { Γ := Γ, rank := m + 1 }-Function₂ F)
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{F : V → V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
(hF : { Γ := Γ, rank := m + 1 }-Function₃ F)
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
(hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₄.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{F : V → V → V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
{f₄ : (Fin k → V) → V}
(hF : { Γ := Γ, rank := m + 1 }-Function₄ F)
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
(hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃)
(hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₅.comp
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{F : V → V → V → V → V → V}
{f₁ : (Fin k → V) → V}
{f₂ : (Fin k → V) → V}
{f₃ : (Fin k → V) → V}
{f₄ : (Fin k → V) → V}
{f₅ : (Fin k → V) → V}
(hF : { Γ := Γ, rank := m + 1 }.BoldfaceFunction₅ F)
(hf₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₁)
(hf₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₂)
(hf₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₃)
(hf₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₄)
(hf₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f₅)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₁
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{f : V → V}
[{ Γ := Γ, rank := m + 1 }-Function₁ f]
{g : (Fin k → V) → V}
(hg : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₂
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{f : V → V → V}
[{ Γ := Γ, rank := m + 1 }-Function₂ f]
{g₁ : (Fin k → V) → V}
{g₂ : (Fin k → V) → V}
(hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁)
(hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₃
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{f : V → V → V → V}
[{ Γ := Γ, rank := m + 1 }-Function₃ f]
{g₁ : (Fin k → V) → V}
{g₂ : (Fin k → V) → V}
{g₃ : (Fin k → V) → V}
(hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁)
(hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂)
(hg₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₃)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₄
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{f : V → V → V → V → V}
[{ Γ := Γ, rank := m + 1 }-Function₄ f]
{g₁ : (Fin k → V) → V}
{g₂ : (Fin k → V) → V}
{g₃ : (Fin k → V) → V}
{g₄ : (Fin k → V) → V}
(hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁)
(hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂)
(hg₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₃)
(hg₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₄)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.comp₅
{V : Type u_2}
[LO.ORingStruc V]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
{k : ℕ}
{f : V → V → V → V → V → V}
[{ Γ := Γ, rank := m + 1 }.BoldfaceFunction₅ f]
{g₁ : (Fin k → V) → V}
{g₂ : (Fin k → V) → V}
{g₃ : (Fin k → V) → V}
{g₄ : (Fin k → V) → V}
{g₅ : (Fin k → V) → V}
(hg₁ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₁)
(hg₂ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₂)
(hg₃ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₃)
(hg₄ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₄)
(hg₅ : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction g₅)
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_lt
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{m : ℕ}
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
(h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_lt
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{m : ℕ}
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
(h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_le
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{m : ℕ}
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
(h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.bex_le
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{m : ℕ}
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
(h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_lt'
{V : Type u_2}
[LO.ORingStruc V]
{k : ℕ}
{m : ℕ}
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
(h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Boldface.ball_le'
{V : Type u_2}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{k : ℕ}
{m : ℕ}
{Γ : LO.SigmaPiDelta}
{P : (Fin k → V) → V → Prop}
{f : (Fin k → V) → V}
(hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f)
(h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succ → V) => P (fun (x : Fin k) => w x.succ) (w 0))
: