Equations
- LO.Arith.sub a b = Classical.choose! ⋯
Instances For
Equations
- LO.Arith.instSub_arithmetization = { sub := LO.Arith.sub }
theorem
LO.Arith.sub_spec_of_ge
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(h : a ≥ b)
:
theorem
LO.Arith.sub_spec_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(h : a < b)
:
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.sub_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
:
𝚺₀-Function₂ fun (x x_1 : V) => x - x_1 via LO.FirstOrder.Arith.subDef
@[simp]
theorem
LO.Arith.sub_defined_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.subDef) ↔ v 0 = v 1 - v 2
instance
LO.Arith.sub_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₂ fun (x x_1 : V) => x - x_1
Equations
- ⋯ = ⋯
instance
LO.Arith.sub_polybounded
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
:
LO.FirstOrder.Arith.Bounded₂ fun (x x_1 : V) => x - x_1
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.sub_spec_of_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(h : a ≤ b)
:
theorem
LO.Arith.sub_add_self_of_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(h : b ≤ a)
:
theorem
LO.Arith.add_tsub_self_of_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(h : b ≤ a)
:
@[simp]
@[simp]
@[simp]
@[simp]
theorem
LO.Arith.sub_remove_left
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
{c : V}
(e : a = b + c)
:
@[simp]
@[simp]
Equations
- ⋯ = ⋯
theorem
LO.Arith.pred_lt_self_of_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
(h : 0 < a)
:
theorem
LO.Arith.le_sub_one_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(h : a < b)
:
theorem
LO.Arith.le_mul_self_of_pos_left
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(hy : 0 < b)
:
theorem
LO.Arith.le_mul_self_of_pos_right
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(hy : 0 < b)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.dvd_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
:
𝚺₀-Relation fun (a b : V) => a ∣ b via LO.FirstOrder.Arith.dvd
@[simp]
instance
LO.Arith.dvd_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.le_of_dvd
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(h : 0 < b)
:
theorem
LO.Arith.not_dvd_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
{a : V}
{b : V}
(pos : 0 < b)
:
@[simp]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.isPrime_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
:
𝚺₀-Predicate fun (a : V) => LO.Arith.IsPrime a via LO.FirstOrder.Arith.isPrime
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.Arith.eval_minDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.min) ↔ v 0 = min (v 1) (v 2)
instance
LO.Arith.min_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₂ min
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.Arith.eval_maxDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.max) ↔ v 0 = max (v 1) (v 2)
instance
LO.Arith.max_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐏𝐀⁻]
(Γ : LO.FirstOrder.Arith.HierarchySymbol)
:
Γ-Function₂ max
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯