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
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
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.
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.
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
- LO.Arith.Fixpoint.Construction.limSeq_definable
- LO.Arith.Fixpoint.Construction.limSeq_definable'
- LO.Arith.Formalized.Numeral.seqExp_definable
- LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqAdd
- LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqEQ
- LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqLT
- LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqMul
- LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNEQ
- LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNLT
- LO.Arith.Formalized.numeral_definable
- LO.Arith.Formalized.numeral_definable'
- LO.Arith.Formalized.substItr_definable
- LO.Arith.Formalized.substItr_definable'
- LO.Arith.Language.Defined.func_definable
- LO.Arith.Language.Defined.func_definable'
- LO.Arith.Language.Defined.rel_definable
- LO.Arith.Language.Defined.rel_definable'
- LO.Arith.Language.TermRec.Construction.graph_definable
- LO.Arith.Language.TermRec.Construction.graph_definable₂
- LO.Arith.Language.Theory.derivable_definable
- LO.Arith.Language.Theory.derivable_definable'
- LO.Arith.Language.Theory.derivationOf_definable
- LO.Arith.Language.Theory.derivationOf_definable'
- LO.Arith.Language.Theory.derivation_definable
- LO.Arith.Language.Theory.derivation_definable'
- LO.Arith.Language.Theory.mem_definable
- LO.Arith.Language.Theory.provable_definable
- LO.Arith.Language.Theory.provable_definable'
- LO.Arith.Language.UformulaRec1.Construction.graph_definable
- LO.Arith.Language.UformulaRec1.Construction.result_definable
- LO.Arith.Language.bv_definable
- LO.Arith.Language.bv_definable'
- LO.Arith.Language.free_definable
- LO.Arith.Language.free_definable'
- LO.Arith.Language.iff_definable
- LO.Arith.Language.iff_definable'
- LO.Arith.Language.imp_definable
- LO.Arith.Language.imp_definable'
- LO.Arith.Language.isFormulaSet_definable
- LO.Arith.Language.isFormulaSet_definable'
- LO.Arith.Language.isSemiformulaDef_definable'
- LO.Arith.Language.isSemiformula_definable
- LO.Arith.Language.isSemitermVec_definable
- LO.Arith.Language.isSemitermVec_defined'
- LO.Arith.Language.isSemiterm_definable
- LO.Arith.Language.isSemiterm_defined'
- LO.Arith.Language.isUFormulaDef_definable
- LO.Arith.Language.isUFormulaDef_definable'
- LO.Arith.Language.isUTermVecDef_definable
- LO.Arith.Language.isUTermVecDef_definable'
- LO.Arith.Language.isUTerm_definable
- LO.Arith.Language.neg_definable
- LO.Arith.Language.neg_definable'
- LO.Arith.Language.qVec_definable
- LO.Arith.Language.qVec_definable'
- LO.Arith.Language.setShift_definable
- LO.Arith.Language.shift_definable
- LO.Arith.Language.substs_definable
- LO.Arith.Language.substs_definable'
- LO.Arith.Language.substs₁_definable
- LO.Arith.Language.termBShiftVec_definable
- LO.Arith.Language.termBShiftVec_definable'
- LO.Arith.Language.termBShift_definable
- LO.Arith.Language.termBShift_definable'
- LO.Arith.Language.termBVVec_definable
- LO.Arith.Language.termBVVec_definable'
- LO.Arith.Language.termBV_definable
- LO.Arith.Language.termBV_definable'
- LO.Arith.Language.termShiftVec_definable
- LO.Arith.Language.termShiftVec_definable'
- LO.Arith.Language.termShift_definable
- LO.Arith.Language.termShift_definable'
- LO.Arith.Language.termSubstVec_definable
- LO.Arith.Language.termSubstVec_definable'
- LO.Arith.Language.termSubst_definable
- LO.Arith.Language.termSubst_definable'
- LO.Arith.Nth.graph_definable
- LO.Arith.Nth.graph_definable'
- LO.Arith.Nuon.ext_Definable
- LO.Arith.Nuon.nuonAux_definable
- LO.Arith.PR.Construction.result_definable
- LO.Arith.PR.Construction.result_definable_delta₁
- LO.Arith.VecRec.Construction.graph_definable
- LO.Arith.VecRec.Construction.graph_definable'
- LO.Arith.VecRec.Construction.graph_definable''
- LO.Arith.VecRec.Construction.result_definable
- LO.Arith.VecRec.Construction.result_definable'
- LO.Arith.bexp_definable
- LO.Arith.bitSubset_definable
- LO.Arith.bitSubset_definable'
- LO.Arith.concat_definable
- LO.Arith.concat_definable'
- LO.Arith.cons_definable
- LO.Arith.cons_definable'
- LO.Arith.div_definable
- LO.Arith.domain_definable
- LO.Arith.domain_definable'
- LO.Arith.dvd_definable
- LO.Arith.exp_definable_deltaZero
- LO.Arith.exponential_definable
- LO.Arith.exponential_definable'
- LO.Arith.ext_definable
- LO.Arith.fbit_definable
- LO.Arith.fstIdx_definable
- LO.Arith.fstIdx_definable'
- LO.Arith.hash_definable
- LO.Arith.insert_definable
- LO.Arith.insert_definable'
- LO.Arith.instBoldfaceFunction₁QqAll
- LO.Arith.instBoldfaceFunction₁QqEx
- LO.Arith.instBoldfaceFunction₂MkHAddNatOfNatSubsts₁
- LO.Arith.instBoldfaceFunction₂QqAnd
- LO.Arith.instBoldfaceFunction₂QqOr
- LO.Arith.instBoldfaceFunction₃QqNRel
- LO.Arith.instBoldfaceFunction₃QqRel
- LO.Arith.isMapping_definable
- LO.Arith.isMapping_definable'
- LO.Arith.isUTermDef_definable'
- LO.Arith.language.shift_definable'
- LO.Arith.len_definable
- LO.Arith.len_definable'
- LO.Arith.lenbit_definable
- LO.Arith.length_definable
- LO.Arith.lh_definable
- LO.Arith.lh_definable'
- LO.Arith.listMax_definable
- LO.Arith.listMax_definable'
- LO.Arith.log_definable
- LO.Arith.max_definable
- LO.Arith.memVec_definable
- LO.Arith.memVec_definable'
- LO.Arith.mem_definable
- LO.Arith.mem_definable'
- LO.Arith.min_definable
- LO.Arith.mkSeq₁_definable
- LO.Arith.mkSeq₁_definable'
- LO.Arith.mkSeq₂_definable
- LO.Arith.mkSeq₂_definable'
- LO.Arith.mkVec₁_definable
- LO.Arith.mkVec₁_definable'
- LO.Arith.mkVec₂_definable
- LO.Arith.mkVec₂_definable'
- LO.Arith.nth_definable
- LO.Arith.nth_definable'
- LO.Arith.nuon_definable
- LO.Arith.pair_definable
- LO.Arith.pi₁_definable
- LO.Arith.pi₂_definable
- LO.Arith.pow2_definable
- LO.Arith.ppow2_definable
- LO.Arith.product_definable
- LO.Arith.product_definable'
- LO.Arith.provableₐ_definable
- LO.Arith.provableₐ_definable'
- LO.Arith.qqConj_definable
- LO.Arith.qqConj_definable'
- LO.Arith.qqDisj_definable
- LO.Arith.qqDisj_definable'
- LO.Arith.qqVerums_definable
- LO.Arith.qqVerums_definable'
- LO.Arith.range_definable
- LO.Arith.range_definable'
- LO.Arith.rem_definable
- LO.Arith.repeatVec_definable
- LO.Arith.repeatVec_definable'
- LO.Arith.sUnion_definable
- LO.Arith.sUnion_definable'
- LO.Arith.seqCons_definable
- LO.Arith.seqCons_definable'
- LO.Arith.seq_definable
- LO.Arith.seq_definable'
- LO.Arith.sndIdx_definable
- LO.Arith.sndIdx_definable'
- LO.Arith.sqrt_definable
- LO.Arith.sub_definable
- LO.Arith.subsetVec_definable
- LO.Arith.subsetVec_definable'
- LO.Arith.takeLast_definable
- LO.Arith.takeLast_definable'
- LO.Arith.unNpair_definable
- LO.Arith.under_definable
- LO.Arith.under_definable'
- LO.Arith.union_definable
- LO.Arith.union_definable'
- LO.Arith.vecToSet_definable
- LO.Arith.vecToSet_definable'
- LO.Arith.znth_definable
- LO.Arith.znth_definable'
- LO.FirstOrder.Arith.HierarchySymbol.Boldface.instMkOfDeltaSigmaPiDelta
- LO.FirstOrder.Arith.HierarchySymbol.Boldface.instOfSigmaZero
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instMkDeltaSigmaPiDeltaOfSigma
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction.instOfSigmaZero
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₁.graph
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.add
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.graph
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.hAdd
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.hMul
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₂.mul
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₃.graph
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.eq
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.le
- LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel.lt
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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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)
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceRel
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(P : V → V → Prop)
:
@[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)
@[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)
@[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)
@[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)
:
@[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)
:
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.BoldfaceFunction₀
{V : Type u_2}
[LO.ORingStruc V]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
(c : V)
:
@[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)
@[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)
@[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)
@[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)
@[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
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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))
: