Documentation

Arithmetization.ISigmaOne.Metamath.Formula.Functions

source
def LO.Arith.Negation.blueprint (pL : FirstOrder.Arith.LDef) :
Language.UformulaRec1.Blueprint pL
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Negation.construction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} :
Language.UformulaRec1.Construction V L (blueprint pL)
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Language.neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
V
Equations
Instances For
source
def LO.FirstOrder.Arith.LDef.negDef (pL : LDef) :
𝚺₁.Semisentence 2
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Language.neg_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₁ L.neg via pL.negDef
source
instance LO.Arith.Language.neg_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₁ L.neg
source
instance LO.Arith.Language.neg_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m : ℕ} (Γ : SigmaPiDelta) :
{ Γ := Γ, rank := m + 1 }-Function₁ L.neg
source
@[simp]
theorem LO.Arith.neg_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
L.neg (qqRel k R v) = qqNRel k R v
source
@[simp]
theorem LO.Arith.neg_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
L.neg (qqNRel k R v) = qqRel k R v
source
@[simp]
theorem LO.Arith.neg_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
L.neg qqVerum = qqFalsum
source
@[simp]
theorem LO.Arith.neg_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
L.neg qqFalsum = qqVerum
source
@[simp]
theorem LO.Arith.neg_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
L.neg (qqAnd p q) = qqOr (L.neg p) (L.neg q)
source
@[simp]
theorem LO.Arith.neg_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
L.neg (qqOr p q) = qqAnd (L.neg p) (L.neg q)
source
@[simp]
theorem LO.Arith.neg_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
L.neg (qqAll p) = qqEx (L.neg p)
source
@[simp]
theorem LO.Arith.neg_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
L.neg (qqEx p) = qqAll (L.neg p)
source
theorem LO.Arith.neg_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {x : V} (h : ¬L.IsUFormula x) :
L.neg x = 0
source
theorem LO.Arith.Language.IsUFormula.neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
L.IsUFormula p → L.IsUFormula (L.neg p)
source
@[simp]
theorem LO.Arith.Language.IsUFormula.bv_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
L.IsUFormula p → L.bv (L.neg p) = L.bv p
source
@[simp]
theorem LO.Arith.Language.IsUFormula.neg_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
L.IsUFormula p → L.neg (L.neg p) = p
source
@[simp]
theorem LO.Arith.Language.IsUFormula.neg_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
L.IsUFormula (L.neg p) ↔ L.IsUFormula p
source
@[simp]
theorem LO.Arith.Language.IsSemiformula.neg_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
L.IsSemiformula n (L.neg p) ↔ L.IsSemiformula n p
source
theorem LO.Arith.Language.IsSemiformula.neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
L.IsSemiformula n p → L.IsSemiformula n (L.neg p)

Alias of the reverse direction of LO.Arith.Language.IsSemiformula.neg_iff.

source
theorem LO.Arith.Language.IsSemiformula.elim_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
L.IsSemiformula n (L.neg p) → L.IsSemiformula n p

Alias of the forward direction of LO.Arith.Language.IsSemiformula.neg_iff.

source
@[simp]
theorem LO.Arith.neg_inj_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
L.neg p = L.neg q ↔ p = q
source
def LO.Arith.Language.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p q : V) :
V
Equations
Instances For
source
def LO.Arith.«term_^→[_]_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Language.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p q : V) :
V
Equations
Instances For
source
@[simp]
theorem LO.Arith.Language.IsUFormula.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} :
L.IsUFormula (p ^→[L] q) ↔ L.IsUFormula p ∧ L.IsUFormula q
source
@[simp]
theorem LO.Arith.Language.IsSemiformula.imp {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p q : V} :
L.IsSemiformula n (p ^→[L] q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q
source
def LO.FirstOrder.Arith.LDef.impDef (pL : LDef) :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Language.imp_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₂ L.imp via pL.impDef
source
instance LO.Arith.Language.imp_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₂ L.imp
source
instance LO.Arith.Language.imp_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
{ Γ := Γ, rank := m + 1 }-Function₂ L.imp
source
@[simp]
theorem LO.Arith.Language.IsUFormula.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} :
L.IsUFormula (L.iff p q) ↔ L.IsUFormula p ∧ L.IsUFormula q
source
@[simp]
theorem LO.Arith.Language.IsSemiformula.iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p q : V} :
L.IsSemiformula n (L.iff p q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q
source
@[simp]
theorem LO.Arith.lt_iff_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p q : V) :
p < L.iff p q
source
@[simp]
theorem LO.Arith.lt_iff_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p q : V) :
q < L.iff p q
source
def LO.FirstOrder.Arith.LDef.qqIffDef (pL : LDef) :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Language.iff_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₂ L.iff via pL.qqIffDef
source
instance LO.Arith.Language.iff_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₂ L.iff
source
instance LO.Arith.Language.iff_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
{ Γ := Γ, rank := m + 1 }-Function₂ L.iff
source
def LO.Arith.Shift.blueprint (pL : FirstOrder.Arith.LDef) :
Language.UformulaRec1.Blueprint pL
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Shift.construction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
Language.UformulaRec1.Construction V L (blueprint pL)
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Language.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
V
Equations
Instances For
source
def LO.FirstOrder.Arith.LDef.shiftDef (pL : LDef) :
𝚺₁.Semisentence 2
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Language.shift_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₁ L.shift via pL.shiftDef
source
instance LO.Arith.Language.shift_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₁ L.shift
source
instance LO.Arith.language.shift_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
{ Γ := Γ, rank := m + 1 }-Function₁ L.shift
source
@[simp]
theorem LO.Arith.shift_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
L.shift (qqRel k R v) = qqRel k R (L.termShiftVec k v)
source
@[simp]
theorem LO.Arith.shift_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
L.shift (qqNRel k R v) = qqNRel k R (L.termShiftVec k v)
source
@[simp]
theorem LO.Arith.shift_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
L.shift qqVerum = qqVerum
source
@[simp]
theorem LO.Arith.shift_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
L.shift qqFalsum = qqFalsum
source
@[simp]
theorem LO.Arith.shift_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
L.shift (qqAnd p q) = qqAnd (L.shift p) (L.shift q)
source
@[simp]
theorem LO.Arith.shift_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
L.shift (qqOr p q) = qqOr (L.shift p) (L.shift q)
source
@[simp]
theorem LO.Arith.shift_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
L.shift (qqAll p) = qqAll (L.shift p)
source
@[simp]
theorem LO.Arith.shift_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) :
L.shift (qqEx p) = qqEx (L.shift p)
source
theorem LO.Arith.shift_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {x : V} (h : ¬L.IsUFormula x) :
L.shift x = 0
source
theorem LO.Arith.Language.IsUFormula.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
L.IsUFormula p → L.IsUFormula (L.shift p)
source
theorem LO.Arith.Language.IsUFormula.bv_shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} :
L.IsUFormula p → L.bv (L.shift p) = L.bv p
source
theorem LO.Arith.Language.IsSemiformula.shift {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
L.IsSemiformula n p → L.IsSemiformula n (L.shift p)
source
@[simp]
theorem LO.Arith.Language.IsSemiformula.shift_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} :
L.IsSemiformula n (L.shift p) ↔ L.IsSemiformula n p
source
theorem LO.Arith.shift_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p : V} (hp : L.IsSemiformula n p) :
L.shift (L.neg p) = L.neg (L.shift p)
source
def LO.FirstOrder.Arith.LDef.qVecDef (pL : LDef) :
𝚺₁.Semisentence 2
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Language.qVec_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₁ L.qVec via pL.qVecDef
source
instance LO.Arith.Language.qVec_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₁ L.qVec
source
instance LO.Arith.Language.qVec_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
{ Γ := Γ, rank := m + 1 }-Function₁ L.qVec
source
def LO.Arith.Substs.blueprint (pL : FirstOrder.Arith.LDef) :
Language.UformulaRec1.Blueprint pL
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Substs.construction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
Language.UformulaRec1.Construction V L (blueprint pL)
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Language.substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (w p : V) :
V
Equations
Instances For
source
def LO.FirstOrder.Arith.LDef.substsDef (pL : LDef) :
𝚺₁.Semisentence 3
Equations
source
theorem LO.Arith.Language.substs_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₂ L.substs via pL.substsDef
source
instance LO.Arith.Language.substs_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₂ L.substs
source
instance LO.Arith.Language.substs_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
{ Γ := Γ, rank := m + 1 }-Function₂ L.substs
source
@[simp]
theorem LO.Arith.substs_rel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
L.substs w (qqRel k R v) = qqRel k R (L.termSubstVec k w v)
source
@[simp]
theorem LO.Arith.substs_nrel {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) :
L.substs w (qqNRel k R v) = qqNRel k R (L.termSubstVec k w v)
source
@[simp]
theorem LO.Arith.substs_verum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (w : V) :
L.substs w qqVerum = qqVerum
source
@[simp]
theorem LO.Arith.substs_falsum {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (w : V) :
L.substs w qqFalsum = qqFalsum
source
@[simp]
theorem LO.Arith.substs_and {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
L.substs w (qqAnd p q) = qqAnd (L.substs w p) (L.substs w q)
source
@[simp]
theorem LO.Arith.substs_or {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) :
L.substs w (qqOr p q) = qqOr (L.substs w p) (L.substs w q)
source
@[simp]
theorem LO.Arith.substs_all {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w p : V} (hp : L.IsUFormula p) :
L.substs w (qqAll p) = qqAll (L.substs (L.qVec w) p)
source
@[simp]
theorem LO.Arith.substs_ex {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w p : V} (hp : L.IsUFormula p) :
L.substs w (qqEx p) = qqEx (L.substs (L.qVec w) p)
source
theorem LO.Arith.isUFormula_subst_induction_sigma1 {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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 (qqRel k R v) (qqRel k R (L.termSubstVec k w v))) (hNRel : ∀ (w k R v : V), L.Rel k R → L.IsUTermVec k v → P w (qqNRel k R v) (qqNRel k R (L.termSubstVec k w v))) (hverum : ∀ (w : V), P w qqVerum qqVerum) (hfalsum : ∀ (w : V), P w qqFalsum 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 (qqAnd p q) (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 (qqOr p q) (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 (qqAll p) (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 (qqEx p) (qqEx (L.substs (L.qVec w) p))) {w p : V} :
L.IsUFormula p → P w p (L.substs w p)
source
theorem LO.Arith.semiformula_subst_induction {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : 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 (qqRel k R v) (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 (qqNRel k R v) (qqNRel k R (L.termSubstVec k w v))) (hverum : ∀ (n w : V), P n w qqVerum qqVerum) (hfalsum : ∀ (n w : V), P n w qqFalsum 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 (qqAnd p q) (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 (qqOr p q) (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 (qqAll p) (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 (qqEx p) (qqEx (L.substs (L.qVec w) p))) {n p w : V} :
L.IsSemiformula n p → P n w p (L.substs w p)
source
@[simp]
theorem LO.Arith.Language.IsSemiformula.substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n p m w : V} :
L.IsSemiformula n p → L.IsSemitermVec n m w → L.IsSemiformula m (L.substs w p)
source
theorem LO.Arith.substs_not_uformula {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {w x : V} (h : ¬L.IsUFormula x) :
L.substs w x = 0
source
theorem LO.Arith.substs_neg {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m w n p : V} (hp : L.IsSemiformula n p) :
L.IsSemitermVec n m w → L.substs w (L.neg p) = L.neg (L.substs w p)
source
theorem LO.Arith.shift_substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m w n 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)
source
theorem LO.Arith.substs_substs {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {m w l n 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
source
theorem LO.Arith.subst_eq_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p n w : V} (hp : L.IsSemiformula n p) (hw : L.IsSemitermVec n n w) (H : ∀ i < n, nth w i = qqBvar i) :
L.substs w p = p
source
theorem LO.Arith.subst_eq_self₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsSemiformula 1 p) :
L.substs ?[qqBvar 0] p = p
source
def LO.Arith.Language.substs₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (t u : V) :
V
Equations
  • L.substs₁ t u = L.substs ?[t] u
Instances For
source
def LO.FirstOrder.Arith.LDef.substs₁Def (pL : LDef) :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Language.substs₁_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₂ L.substs₁ via pL.substs₁Def
source
instance LO.Arith.Language.substs₁_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₂ L.substs₁
source
instance LO.Arith.instBoldfaceFunction₂MkHAddNatOfNatSubsts₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
{ Γ := Γ, rank := m + 1 }-Function₂ L.substs₁
source
theorem LO.Arith.Language.IsSemiformula.substs₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n t p : V} (ht : L.IsSemiterm n t) (hp : L.IsSemiformula 1 p) :
L.IsSemiformula n (L.substs₁ t p)
source
def LO.Arith.Language.free {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : V) :
V
Equations
Instances For
source
def LO.FirstOrder.Arith.LDef.freeDef (pL : LDef) :
𝚺₁.Semisentence 2
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Language.free_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₁ L.free via pL.freeDef
source
instance LO.Arith.Language.free_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] :
𝚺₁-Function₁ L.free
source
instance LO.Arith.Language.free_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} :
{ Γ := Γ, rank := m + 1 }-Function₁ L.free
source
@[simp]
theorem LO.Arith.Language.IsSemiformula.free {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsSemiformula 1 p) :
L.IsFormula (L.free p)
source
def LO.Arith.Formalized.qqEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
V
Equations
Instances For
source
def LO.Arith.Formalized.qqNEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
V
Equations
Instances For
source
def LO.Arith.Formalized.qqLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
V
Equations
Instances For
source
def LO.Arith.Formalized.qqNLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
V
Equations
Instances For
source
def LO.Arith.Formalized.«term_^=_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Formalized.«term_^≠_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Formalized.«term_^<_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.Arith.Formalized.«term_^≮_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem LO.Arith.Formalized.lt_qqEQ_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
x < x ^= y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqEQ_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
y < x ^= y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqLT_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
x < x ^< y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqLT_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
y < x ^< y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqNEQ_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
x < x ^≠ y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqNEQ_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
y < x ^≠ y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqNLT_left {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
x < x ^≮ y
source
@[simp]
theorem LO.Arith.Formalized.lt_qqNLT_right {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (x y : V) :
y < x ^≮ y
source
def LO.FirstOrder.Arith.qqEQDef :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.FirstOrder.Arith.qqNEQDef :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.FirstOrder.Arith.qqLTDef :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.FirstOrder.Arith.qqNLTDef :
𝚺₁.Semisentence 3
Equations
  • One or more equations did not get rendered due to their size.
source
theorem LO.Arith.Formalized.qqEQ_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₂ qqEQ via FirstOrder.Arith.qqEQDef
source
theorem LO.Arith.Formalized.qqNEQ_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₂ qqNEQ via FirstOrder.Arith.qqNEQDef
source
theorem LO.Arith.Formalized.qqLT_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₂ qqLT via FirstOrder.Arith.qqLTDef
source
theorem LO.Arith.Formalized.qqNLT_defined {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
𝚺₁-Function₂ qqNLT via FirstOrder.Arith.qqNLTDef
source
instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) :
{ Γ := Γ, rank := m + 1 }-Function₂ qqEQ
source
instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNEQ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) :
{ Γ := Γ, rank := m + 1 }-Function₂ qqNEQ
source
instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) :
{ Γ := Γ, rank := m + 1 }-Function₂ qqLT
source
instance LO.Arith.Formalized.instBoldfaceFunction₂MkHAddNatOfNatQqNLT {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) :
{ Γ := Γ, rank := m + 1 }-Function₂ qqNLT
source
@[simp]
theorem LO.Arith.Formalized.eval_qqEQDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :
V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqEQDef) ↔ v 0 = v 1 ^= v 2
source
@[simp]
theorem LO.Arith.Formalized.eval_qqNEQDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :
V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqNEQDef) ↔ v 0 = v 1 ^≠ v 2
source
@[simp]
theorem LO.Arith.Formalized.eval_qqLTDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :
V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqLTDef) ↔ v 0 = v 1 ^< v 2
source
@[simp]
theorem LO.Arith.Formalized.eval_qqNLTDef {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) :
V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.qqNLTDef) ↔ v 0 = v 1 ^≮ v 2
source
theorem LO.Arith.Formalized.neg_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
⌜ℒₒᵣ⌝.neg (t ^= u) = t ^≠ u
source
theorem LO.Arith.Formalized.neg_neq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
⌜ℒₒᵣ⌝.neg (t ^≠ u) = t ^= u
source
theorem LO.Arith.Formalized.neg_lt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
⌜ℒₒᵣ⌝.neg (t ^< u) = t ^≮ u
source
theorem LO.Arith.Formalized.neg_nlt {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
⌜ℒₒᵣ⌝.neg (t ^≮ u) = t ^< u
source
theorem LO.Arith.Formalized.substs_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {w t u : V} (ht : ⌜ℒₒᵣ⌝.IsUTerm t) (hu : ⌜ℒₒᵣ⌝.IsUTerm u) :
⌜ℒₒᵣ⌝.substs w (t ^= u) = ⌜ℒₒᵣ⌝.termSubst w t ^= ⌜ℒₒᵣ⌝.termSubst w u