Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Negation.construction
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.neg
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : V)
:
V
Equations
- L.neg p = (LO.Arith.Negation.construction L).result 0 p
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.neg_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.neg via pL.negDef
instance
LO.Arith.Language.neg_definable
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.neg
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.neg_definable'
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{m : ℕ}
(Γ : LO.SigmaPiDelta)
:
{ Γ := Γ, rank := m + 1 }-Function₁ L.neg
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.neg_rel
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
L.neg (LO.Arith.qqRel k R v) = LO.Arith.qqNRel k R v
@[simp]
theorem
LO.Arith.neg_nrel
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
L.neg (LO.Arith.qqNRel k R v) = LO.Arith.qqRel k R v
@[simp]
theorem
LO.Arith.neg_verum
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
L.neg LO.Arith.qqVerum = LO.Arith.qqFalsum
@[simp]
theorem
LO.Arith.neg_falsum
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
L.neg LO.Arith.qqFalsum = LO.Arith.qqVerum
@[simp]
theorem
LO.Arith.neg_and
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
L.neg (LO.Arith.qqAnd p q) = LO.Arith.qqOr (L.neg p) (L.neg q)
@[simp]
theorem
LO.Arith.neg_or
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
L.neg (LO.Arith.qqOr p q) = LO.Arith.qqAnd (L.neg p) (L.neg q)
@[simp]
theorem
LO.Arith.neg_all
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(hp : L.IsUFormula p)
:
L.neg (LO.Arith.qqAll p) = LO.Arith.qqEx (L.neg p)
@[simp]
theorem
LO.Arith.neg_ex
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(hp : L.IsUFormula p)
:
L.neg (LO.Arith.qqEx p) = LO.Arith.qqAll (L.neg p)
theorem
LO.Arith.neg_not_uformula
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{x : V}
(h : ¬L.IsUFormula x)
:
L.neg x = 0
theorem
LO.Arith.Language.IsUFormula.neg
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula p → L.IsUFormula (L.neg p)
@[simp]
theorem
LO.Arith.Language.IsUFormula.bv_neg
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula p → L.bv (L.neg p) = L.bv p
@[simp]
theorem
LO.Arith.Language.IsUFormula.neg_neg
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula p → L.neg (L.neg p) = p
@[simp]
theorem
LO.Arith.Language.IsUFormula.neg_iff
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula (L.neg p) ↔ L.IsUFormula p
@[simp]
theorem
LO.Arith.Language.IsSemiformula.neg_iff
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
:
L.IsSemiformula n (L.neg p) ↔ L.IsSemiformula n p
theorem
LO.Arith.Language.IsSemiformula.neg
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
:
L.IsSemiformula n p → L.IsSemiformula n (L.neg p)
Alias of the reverse direction of LO.Arith.Language.IsSemiformula.neg_iff
.
theorem
LO.Arith.Language.IsSemiformula.elim_neg
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
:
L.IsSemiformula n (L.neg p) → L.IsSemiformula n p
Alias of the forward direction of LO.Arith.Language.IsSemiformula.neg_iff
.
@[simp]
theorem
LO.Arith.neg_inj_iff
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
def
LO.Arith.Language.imp
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : V)
(q : V)
:
V
Equations
- p ^→[L] q = LO.Arith.qqOr (L.neg p) q
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.iff
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : V)
(q : V)
:
V
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.imp_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₂ L.imp via pL.impDef
instance
LO.Arith.Language.imp_definable
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₂ L.imp
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.imp_definable'
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }-Function₂ L.imp
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.Language.IsUFormula.iff
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
:
@[simp]
theorem
LO.Arith.Language.IsSemiformula.iff
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
{q : V}
:
@[simp]
theorem
LO.Arith.lt_iff_left
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : V)
(q : V)
:
p < L.iff p q
@[simp]
theorem
LO.Arith.lt_iff_right
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : V)
(q : V)
:
q < L.iff p q
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.iff_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₂ L.iff via pL.qqIffDef
instance
LO.Arith.Language.iff_definable
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₂ L.iff
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.iff_definable'
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }-Function₂ L.iff
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Shift.construction
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.shift
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : V)
:
V
Equations
- L.shift p = (LO.Arith.Shift.construction L).result 0 p
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.shift_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.shift via pL.shiftDef
instance
LO.Arith.Language.shift_definable
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.shift
Equations
- ⋯ = ⋯
instance
LO.Arith.language.shift_definable'
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }-Function₁ L.shift
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.shift_rel
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
L.shift (LO.Arith.qqRel k R v) = LO.Arith.qqRel k R (L.termShiftVec k v)
@[simp]
theorem
LO.Arith.shift_nrel
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
L.shift (LO.Arith.qqNRel k R v) = LO.Arith.qqNRel k R (L.termShiftVec k v)
@[simp]
theorem
LO.Arith.shift_verum
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
L.shift LO.Arith.qqVerum = LO.Arith.qqVerum
@[simp]
theorem
LO.Arith.shift_falsum
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
L.shift LO.Arith.qqFalsum = LO.Arith.qqFalsum
@[simp]
theorem
LO.Arith.shift_and
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
L.shift (LO.Arith.qqAnd p q) = LO.Arith.qqAnd (L.shift p) (L.shift q)
@[simp]
theorem
LO.Arith.shift_or
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
L.shift (LO.Arith.qqOr p q) = LO.Arith.qqOr (L.shift p) (L.shift q)
@[simp]
theorem
LO.Arith.shift_all
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(hp : L.IsUFormula p)
:
L.shift (LO.Arith.qqAll p) = LO.Arith.qqAll (L.shift p)
@[simp]
theorem
LO.Arith.shift_ex
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(hp : L.IsUFormula p)
:
L.shift (LO.Arith.qqEx p) = LO.Arith.qqEx (L.shift p)
theorem
LO.Arith.shift_not_uformula
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{x : V}
(h : ¬L.IsUFormula x)
:
L.shift x = 0
theorem
LO.Arith.Language.IsUFormula.shift
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula p → L.IsUFormula (L.shift p)
theorem
LO.Arith.Language.IsUFormula.bv_shift
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula p → L.bv (L.shift p) = L.bv p
theorem
LO.Arith.Language.IsSemiformula.shift
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
:
L.IsSemiformula n p → L.IsSemiformula n (L.shift p)
@[simp]
theorem
LO.Arith.Language.IsSemiformula.shift_iff
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
:
L.IsSemiformula n (L.shift p) ↔ L.IsSemiformula n p
theorem
LO.Arith.shift_neg
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
(hp : L.IsSemiformula n p)
:
L.shift (L.neg p) = L.neg (L.shift p)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.qVec_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.qVec via pL.qVecDef
instance
LO.Arith.Language.qVec_definable
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.qVec
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.qVec_definable'
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }-Function₁ L.qVec
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Substs.construction
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.substs
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(w : V)
(p : V)
:
V
Equations
- L.substs w p = (LO.Arith.Substs.construction L).result w p
Instances For
Equations
- pL.substsDef = (LO.Arith.Substs.blueprint pL).result
Instances For
theorem
LO.Arith.Language.substs_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₂ L.substs via pL.substsDef
instance
LO.Arith.Language.substs_definable
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₂ L.substs
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.substs_definable'
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }-Function₂ L.substs
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.substs_rel
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{w : V}
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
L.substs w (LO.Arith.qqRel k R v) = LO.Arith.qqRel k R (L.termSubstVec k w v)
@[simp]
theorem
LO.Arith.substs_nrel
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{w : V}
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
L.substs w (LO.Arith.qqNRel k R v) = LO.Arith.qqNRel k R (L.termSubstVec k w v)
@[simp]
theorem
LO.Arith.substs_verum
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(w : V)
:
L.substs w LO.Arith.qqVerum = LO.Arith.qqVerum
@[simp]
theorem
LO.Arith.substs_falsum
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(w : V)
:
L.substs w LO.Arith.qqFalsum = LO.Arith.qqFalsum
@[simp]
theorem
LO.Arith.substs_and
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{w : V}
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
L.substs w (LO.Arith.qqAnd p q) = LO.Arith.qqAnd (L.substs w p) (L.substs w q)
@[simp]
theorem
LO.Arith.substs_or
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{w : V}
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
L.substs w (LO.Arith.qqOr p q) = LO.Arith.qqOr (L.substs w p) (L.substs w q)
@[simp]
theorem
LO.Arith.substs_all
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{w : V}
{p : V}
(hp : L.IsUFormula p)
:
L.substs w (LO.Arith.qqAll p) = LO.Arith.qqAll (L.substs (L.qVec w) p)
@[simp]
theorem
LO.Arith.substs_ex
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{w : V}
{p : V}
(hp : L.IsUFormula p)
:
L.substs w (LO.Arith.qqEx p) = LO.Arith.qqEx (L.substs (L.qVec w) p)
theorem
LO.Arith.isUFormula_subst_induction_sigma1
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{P : V → V → V → Prop}
(hP : 𝚺₁-Relation₃ P)
(hRel : ∀ (w k R v : V), L.Rel k R → L.IsUTermVec k v → P w (LO.Arith.qqRel k R v) (LO.Arith.qqRel k R (L.termSubstVec k w v)))
(hNRel : ∀ (w k R v : V), L.Rel k R → L.IsUTermVec k v → P w (LO.Arith.qqNRel k R v) (LO.Arith.qqNRel k R (L.termSubstVec k w v)))
(hverum : ∀ (w : V), P w LO.Arith.qqVerum LO.Arith.qqVerum)
(hfalsum : ∀ (w : V), P w LO.Arith.qqFalsum LO.Arith.qqFalsum)
(hand : ∀ (w p q : V),
L.IsUFormula p →
L.IsUFormula q →
P w p (L.substs w p) →
P w q (L.substs w q) → P w (LO.Arith.qqAnd p q) (LO.Arith.qqAnd (L.substs w p) (L.substs w q)))
(hor : ∀ (w p q : V),
L.IsUFormula p →
L.IsUFormula q →
P w p (L.substs w p) →
P w q (L.substs w q) → P w (LO.Arith.qqOr p q) (LO.Arith.qqOr (L.substs w p) (L.substs w q)))
(hall : ∀ (w p : V),
L.IsUFormula p →
P (L.qVec w) p (L.substs (L.qVec w) p) → P w (LO.Arith.qqAll p) (LO.Arith.qqAll (L.substs (L.qVec w) p)))
(hex : ∀ (w p : V),
L.IsUFormula p →
P (L.qVec w) p (L.substs (L.qVec w) p) → P w (LO.Arith.qqEx p) (LO.Arith.qqEx (L.substs (L.qVec w) p)))
{w : V}
{p : V}
:
L.IsUFormula p → P w p (L.substs w p)
theorem
LO.Arith.semiformula_subst_induction
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{P : V → V → V → V → Prop}
(hP : 𝚺₁-Relation₄ P)
(hRel : ∀ (n w k R v : V),
L.Rel k R → L.IsSemitermVec k n v → P n w (LO.Arith.qqRel k R v) (LO.Arith.qqRel k R (L.termSubstVec k w v)))
(hNRel : ∀ (n w k R v : V),
L.Rel k R → L.IsSemitermVec k n v → P n w (LO.Arith.qqNRel k R v) (LO.Arith.qqNRel k R (L.termSubstVec k w v)))
(hverum : ∀ (n w : V), P n w LO.Arith.qqVerum LO.Arith.qqVerum)
(hfalsum : ∀ (n w : V), P n w LO.Arith.qqFalsum LO.Arith.qqFalsum)
(hand : ∀ (n w p q : V),
L.IsSemiformula n p →
L.IsSemiformula n q →
P n w p (L.substs w p) →
P n w q (L.substs w q) → P n w (LO.Arith.qqAnd p q) (LO.Arith.qqAnd (L.substs w p) (L.substs w q)))
(hor : ∀ (n w p q : V),
L.IsSemiformula n p →
L.IsSemiformula n q →
P n w p (L.substs w p) →
P n w q (L.substs w q) → P n w (LO.Arith.qqOr p q) (LO.Arith.qqOr (L.substs w p) (L.substs w q)))
(hall : ∀ (n w p : V),
L.IsSemiformula (n + 1) p →
P (n + 1) (L.qVec w) p (L.substs (L.qVec w) p) → P n w (LO.Arith.qqAll p) (LO.Arith.qqAll (L.substs (L.qVec w) p)))
(hex : ∀ (n w p : V),
L.IsSemiformula (n + 1) p →
P (n + 1) (L.qVec w) p (L.substs (L.qVec w) p) → P n w (LO.Arith.qqEx p) (LO.Arith.qqEx (L.substs (L.qVec w) p)))
{n : V}
{p : V}
{w : V}
:
L.IsSemiformula n p → P n w p (L.substs w p)
@[simp]
theorem
LO.Arith.Language.IsSemiformula.substs
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
{m : V}
{w : V}
:
L.IsSemiformula n p → L.IsSemitermVec n m w → L.IsSemiformula m (L.substs w p)
theorem
LO.Arith.substs_not_uformula
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{w : V}
{x : V}
(h : ¬L.IsUFormula x)
:
L.substs w x = 0
theorem
LO.Arith.substs_neg
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{m : V}
{w : V}
{n : V}
{p : V}
(hp : L.IsSemiformula n p)
:
L.IsSemitermVec n m w → L.substs w (L.neg p) = L.neg (L.substs w p)
theorem
LO.Arith.shift_substs
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{m : V}
{w : V}
{n : V}
{p : V}
(hp : L.IsSemiformula n p)
:
L.IsSemitermVec n m w → L.shift (L.substs w p) = L.substs (L.termShiftVec n w) (L.shift p)
theorem
LO.Arith.substs_substs
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{m : V}
{w : V}
{l : V}
{n : V}
{v : V}
{p : V}
(hp : L.IsSemiformula l p)
:
L.IsSemitermVec n m w → L.IsSemitermVec l n v → L.substs w (L.substs v p) = L.substs (L.termSubstVec l w v) p
theorem
LO.Arith.subst_eq_self
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{n : V}
{w : V}
(hp : L.IsSemiformula n p)
(hw : L.IsSemitermVec n n w)
(H : ∀ i < n, LO.Arith.nth w i = LO.Arith.qqBvar i)
:
L.substs w p = p
theorem
LO.Arith.subst_eq_self₁
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(hp : L.IsSemiformula 1 p)
:
L.substs ?[LO.Arith.qqBvar 0] p = p
def
LO.Arith.Language.substs₁
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(t : V)
(u : V)
:
V
Equations
- L.substs₁ t u = L.substs ?[t] u
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.substs₁_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₂ L.substs₁ via pL.substs₁Def
instance
LO.Arith.Language.substs₁_definable
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₂ L.substs₁
Equations
- ⋯ = ⋯
instance
LO.Arith.instBoldfaceFunction₂MkHAddNatOfNatSubsts₁
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }-Function₂ L.substs₁
Equations
- ⋯ = ⋯
theorem
LO.Arith.Language.IsSemiformula.substs₁
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{t : V}
{p : V}
(ht : L.IsSemiterm n t)
(hp : L.IsSemiformula 1 p)
:
L.IsSemiformula n (L.substs₁ t p)
def
LO.Arith.Language.free
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : V)
:
V
Equations
- L.free p = L.substs₁ (LO.Arith.qqFvar 0) (L.shift p)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.free_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.free via pL.freeDef
instance
LO.Arith.Language.free_definable
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.free
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.free_definable'
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }-Function₁ L.free
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.Language.IsSemiformula.free
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(hp : L.IsSemiformula 1 p)
:
L.IsFormula (L.free p)
def
LO.Arith.Formalized.qqEQ
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(y : V)
:
V
Equations
- x ^= y = LO.Arith.qqRel 2 ↑LO.Arith.Formalized.eqIndex ?[x, y]
Instances For
def
LO.Arith.Formalized.qqNEQ
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(y : V)
:
V
Equations
- x ^≠ y = LO.Arith.qqNRel 2 ↑LO.Arith.Formalized.eqIndex ?[x, y]
Instances For
def
LO.Arith.Formalized.qqLT
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(y : V)
:
V
Equations
- x ^< y = LO.Arith.qqRel 2 ↑LO.Arith.Formalized.ltIndex ?[x, y]
Instances For
def
LO.Arith.Formalized.qqNLT
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
(y : V)
:
V
Equations
- x ^≮ y = LO.Arith.qqNRel 2 ↑LO.Arith.Formalized.ltIndex ?[x, y]
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.Arith.Formalized.qqEQ_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.Formalized.qqEQ via LO.FirstOrder.Arith.qqEQDef
theorem
LO.Arith.Formalized.qqNEQ_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.Formalized.qqNEQ via LO.FirstOrder.Arith.qqNEQDef
theorem
LO.Arith.Formalized.qqLT_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.Formalized.qqLT via LO.FirstOrder.Arith.qqLTDef
theorem
LO.Arith.Formalized.qqNLT_defined
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₁-Function₂ LO.Arith.Formalized.qqNLT via LO.FirstOrder.Arith.qqNLTDef
instance
LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqEQ
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqEQ
Equations
- ⋯ = ⋯
instance
LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNEQ
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqNEQ
Equations
- ⋯ = ⋯
instance
LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqLT
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqLT
Equations
- ⋯ = ⋯
instance
LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNLT
{V : Type u_1}
[Zero V]
[One V]
[Add V]
[Mul V]
[LT V]
[V ⊧ₘ* 𝐈𝚺₁]
(Γ : LO.SigmaPiDelta)
(m : ℕ)
:
{ Γ := Γ, rank := m + 1 }-Function₂ LO.Arith.Formalized.qqNLT
Equations
- ⋯ = ⋯