Equations
- LO.Arith.ext u z = z / u % u
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.ext_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₂ fun (a b : V) => LO.Arith.ext a b via LO.FirstOrder.Arith.extDef
instance
LO.Arith.ext_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Function₂ LO.Arith.ext
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.ext_le_add
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(u : V)
(z : V)
:
LO.Arith.ext u z ≤ z
instance
LO.Arith.instBounded₂Ext
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
LO.FirstOrder.Arith.Bounded₂ LO.Arith.ext
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.ext_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{u : V}
(z : V)
(pos : 0 < u)
:
LO.Arith.ext u z < u
theorem
LO.Arith.ext_add_of_dvd_sq_right
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{u : V}
{z₁ : V}
{z₂ : V}
(pos : 0 < u)
(h : u ^ 2 ∣ z₂)
:
LO.Arith.ext u (z₁ + z₂) = LO.Arith.ext u z₁
theorem
LO.Arith.ext_add_of_dvd_sq_left
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{u : V}
{z₁ : V}
{z₂ : V}
(pos : 0 < u)
(h : u ^ 2 ∣ z₁)
:
LO.Arith.ext u (z₁ + z₂) = LO.Arith.ext u z₂
theorem
LO.Arith.ext_rem
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{i : V}
{j : V}
{z : V}
(ppi : LO.Arith.PPow2 i)
(ppj : LO.Arith.PPow2 j)
(hij : i < j)
:
LO.Arith.ext i (z % j) = LO.Arith.ext i z
Equations
- LO.Arith.Exponential.Seq₀ X Y = (LO.Arith.ext 4 X = 1 ∧ LO.Arith.ext 4 Y = 2)
Instances For
def
LO.Arith.Exponential.Seqₛ.Even
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(X : V)
(Y : V)
(u : V)
:
Equations
- LO.Arith.Exponential.Seqₛ.Even X Y u = (LO.Arith.ext (u ^ 2) X = 2 * LO.Arith.ext u X ∧ LO.Arith.ext (u ^ 2) Y = LO.Arith.ext u Y ^ 2)
Instances For
def
LO.Arith.Exponential.Seqₛ.Odd
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(X : V)
(Y : V)
(u : V)
:
Equations
- LO.Arith.Exponential.Seqₛ.Odd X Y u = (LO.Arith.ext (u ^ 2) X = 2 * LO.Arith.ext u X + 1 ∧ LO.Arith.ext (u ^ 2) Y = 2 * LO.Arith.ext u Y ^ 2)
Instances For
def
LO.Arith.Exponential.Seqₛ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(y : V)
(X : V)
(Y : V)
:
Equations
- LO.Arith.Exponential.Seqₛ y X Y = ∀ u ≤ y, u ≠ 2 → LO.Arith.PPow2 u → LO.Arith.Exponential.Seqₛ.Even X Y u ∨ LO.Arith.Exponential.Seqₛ.Odd X Y u
Instances For
def
LO.Arith.Exponential.Seqₘ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(x : V)
(y : V)
(X : V)
(Y : V)
:
Equations
- LO.Arith.Exponential.Seqₘ x y X Y = ∃ u ≤ y ^ 2, u ≠ 2 ∧ LO.Arith.PPow2 u ∧ LO.Arith.ext u X = x ∧ LO.Arith.ext u Y = y
Instances For
Equations
- LO.Arith.Exponential x y = (x = 0 ∧ y = 1 ∨ ∃ X ≤ y ^ 4, ∃ Y ≤ y ^ 4, LO.Arith.Exponential.Seq₀ X Y ∧ LO.Arith.Exponential.Seqₛ y X Y ∧ LO.Arith.Exponential.Seqₘ x y X Y)
Instances For
theorem
LO.Arith.Exponential.Seqₛ.iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(y : V)
(X : V)
(Y : V)
:
LO.Arith.Exponential.Seqₛ y X Y ↔ ∀ u ≤ y,
u ≠ 2 →
LO.Arith.PPow2 u →
((∃ ext_u_X ≤ X, ext_u_X = LO.Arith.ext u X ∧ 2 * ext_u_X = LO.Arith.ext (u ^ 2) X) ∧ ∃ ext_u_Y ≤ Y, ext_u_Y = LO.Arith.ext u Y ∧ ext_u_Y ^ 2 = LO.Arith.ext (u ^ 2) Y) ∨ (∃ ext_u_X ≤ X, ext_u_X = LO.Arith.ext u X ∧ 2 * ext_u_X + 1 = LO.Arith.ext (u ^ 2) X) ∧ ∃ ext_u_Y ≤ Y, ext_u_Y = LO.Arith.ext u Y ∧ 2 * ext_u_Y ^ 2 = LO.Arith.ext (u ^ 2) Y
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Exponential.Seqₛ.defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Relation₃ LO.Arith.Exponential.Seqₛ via LO.Arith.Exponential.Seqₛ.def
theorem
LO.Arith.Exponential.graph_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(x : V)
(y : V)
:
LO.Arith.Exponential x y ↔ x = 0 ∧ y = 1 ∨ ∃ X ≤ y ^ 4,
∃ Y ≤ y ^ 4,
(1 = LO.Arith.ext 4 X ∧ 2 = LO.Arith.ext 4 Y) ∧ LO.Arith.Exponential.Seqₛ y X Y ∧ ∃ u ≤ y ^ 2, u ≠ 2 ∧ LO.Arith.PPow2 u ∧ x = LO.Arith.ext u X ∧ y = LO.Arith.ext u Y
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Exponential.defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
𝚺₀-Relation LO.Arith.Exponential via LO.FirstOrder.Arith.exponentialDef
@[simp]
theorem
LO.Arith.exponential_defined_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(v : Fin 2 → V)
:
Equations
- ⋯ = ⋯
@[simp]
instance
LO.Arith.exponential_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(Γ : LO.FirstOrder.Arith.HierarchySymbol)
:
Γ-Relation LO.Arith.Exponential
Equations
- ⋯ = ⋯
Equations
- LO.Arith.Exponential.seqX₀ = 4
Instances For
Instances For
theorem
LO.Arith.Exponential.seq₀_zero_two
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
LO.Arith.Exponential.Seq₀ LO.Arith.Exponential.seqX₀ LO.Arith.Exponential.seqY₀
theorem
LO.Arith.Exponential.Seq₀.rem
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{X : V}
{Y : V}
{i : V}
(h : LO.Arith.Exponential.Seq₀ X Y)
(ppi : LO.Arith.PPow2 i)
(hi : 4 < i)
:
LO.Arith.Exponential.Seq₀ (X % i) (Y % i)
theorem
LO.Arith.Exponential.Seqₛ.rem
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
{y' : V}
{X : V}
{Y : V}
{i : V}
(h : LO.Arith.Exponential.Seqₛ y X Y)
(ppi : LO.Arith.PPow2 i)
(hi : y' ^ 2 < i)
(hy : y' ≤ y)
:
LO.Arith.Exponential.Seqₛ y' (X % i) (Y % i)
theorem
LO.Arith.Exponential.seqₛ_one_zero_two
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
:
LO.Arith.Exponential.Seqₛ 1 LO.Arith.Exponential.seqX₀ LO.Arith.Exponential.seqY₀
def
LO.Arith.Exponential.append
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(i : V)
(X : V)
(z : V)
:
V
Equations
- LO.Arith.Exponential.append i X z = X % i + z * i
Instances For
theorem
LO.Arith.Exponential.append_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(i : V)
(X : V)
{z : V}
(hz : z < i)
:
LO.Arith.Exponential.append i X z < i ^ 2
theorem
LO.Arith.Exponential.ext_append_last
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
(i : V)
(X : V)
{z : V}
(hz : z < i)
:
LO.Arith.ext i (LO.Arith.Exponential.append i X z) = z
theorem
LO.Arith.Exponential.ext_append_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{i : V}
{j : V}
(hi : LO.Arith.PPow2 i)
(hj : LO.Arith.PPow2 j)
(hij : i < j)
(X : V)
(z : V)
:
LO.Arith.ext i (LO.Arith.Exponential.append j X z) = LO.Arith.ext i X
theorem
LO.Arith.Exponential.Seq₀.append
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{X : V}
{Y : V}
{i : V}
{x : V}
{y : V}
(H : LO.Arith.Exponential.Seq₀ X Y)
(ppi : LO.Arith.PPow2 i)
(hi : 4 < i)
:
theorem
LO.Arith.Exponential.Seqₛ.append
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{z : V}
{x : V}
{y : V}
{X : V}
{Y : V}
{i : V}
(h : LO.Arith.Exponential.Seqₛ z X Y)
(ppi : LO.Arith.PPow2 i)
(hz : z < i)
:
LO.Arith.Exponential.Seqₛ z (LO.Arith.Exponential.append (i ^ 2) X x) (LO.Arith.Exponential.append (i ^ 2) Y y)
@[simp]
@[simp]
theorem
LO.Arith.Exponential.pow2_ext_of_seq₀_of_seqₛ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
{X : V}
{Y : V}
(h₀ : LO.Arith.Exponential.Seq₀ X Y)
(hₛ : LO.Arith.Exponential.Seqₛ y X Y)
{i : V}
(ne2 : i ≠ 2)
(hi : i ≤ y ^ 2)
(ppi : LO.Arith.PPow2 i)
:
LO.Arith.Pow2 (LO.Arith.ext i Y)
theorem
LO.Arith.Exponential.range_pow2
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(h : LO.Arith.Exponential x y)
:
theorem
LO.Arith.Exponential.le_sq_ext_of_seq₀_of_seqₛ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
{X : V}
{Y : V}
(h₀ : LO.Arith.Exponential.Seq₀ X Y)
(hₛ : LO.Arith.Exponential.Seqₛ y X Y)
{i : V}
(ne2 : i ≠ 2)
(hi : i ≤ y ^ 2)
(ppi : LO.Arith.PPow2 i)
:
i ≤ LO.Arith.ext i Y ^ 2
theorem
LO.Arith.Exponential.two_mul_ext_le_of_seq₀_of_seqₛ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
{X : V}
{Y : V}
(h₀ : LO.Arith.Exponential.Seq₀ X Y)
(hₛ : LO.Arith.Exponential.Seqₛ y X Y)
{i : V}
(ne2 : i ≠ 2)
(hi : i ≤ y ^ 2)
(ppi : LO.Arith.PPow2 i)
:
2 * LO.Arith.ext i Y ≤ i
theorem
LO.Arith.Exponential.exponential_exists_sq_of_exponential_even
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential (2 * x) y → ∃ (y' : V), y = y' ^ 2 ∧ LO.Arith.Exponential x y'
theorem
LO.Arith.Exponential.bit_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential x y → LO.Arith.Exponential (2 * x) (y ^ 2)
theorem
LO.Arith.Exponential.exponential_even
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential (2 * x) y ↔ ∃ (y' : V), y = y' ^ 2 ∧ LO.Arith.Exponential x y'
theorem
LO.Arith.Exponential.exponential_even_sq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential (2 * x) (y ^ 2) ↔ LO.Arith.Exponential x y
theorem
LO.Arith.Exponential.exponential_exists_sq_of_exponential_odd
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential (2 * x + 1) y → ∃ (y' : V), y = 2 * y' ^ 2 ∧ LO.Arith.Exponential x y'
theorem
LO.Arith.Exponential.bit_one
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential x y → LO.Arith.Exponential (2 * x + 1) (2 * y ^ 2)
theorem
LO.Arith.Exponential.exponential_odd
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential (2 * x + 1) y ↔ ∃ (y' : V), y = 2 * y' ^ 2 ∧ LO.Arith.Exponential x y'
theorem
LO.Arith.Exponential.exponential_odd_two_mul_sq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential (2 * x + 1) (2 * y ^ 2) ↔ LO.Arith.Exponential x y
theorem
LO.Arith.Exponential.two_le_ext_of_seq₀_of_seqₛ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
{X : V}
{Y : V}
(h₀ : LO.Arith.Exponential.Seq₀ X Y)
(hₛ : LO.Arith.Exponential.Seqₛ y X Y)
{i : V}
(ne2 : i ≠ 2)
(hi : i ≤ y ^ 2)
(ppi : LO.Arith.PPow2 i)
:
2 ≤ LO.Arith.ext i Y
theorem
LO.Arith.Exponential.ext_le_ext_of_seq₀_of_seqₛ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
{X : V}
{Y : V}
(h₀ : LO.Arith.Exponential.Seq₀ X Y)
(hₛ : LO.Arith.Exponential.Seqₛ y X Y)
{i : V}
(ne2 : i ≠ 2)
(hi : i ≤ y ^ 2)
(ppi : LO.Arith.PPow2 i)
:
LO.Arith.ext i X < LO.Arith.ext i Y
theorem
LO.Arith.Exponential.range_pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(h : LO.Arith.Exponential x y)
:
0 < y
theorem
LO.Arith.Exponential.lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(h : LO.Arith.Exponential x y)
:
x < y
theorem
LO.Arith.Exponential.not_exponential_of_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(h : x ≤ y)
:
@[simp]
@[simp]
theorem
LO.Arith.Exponential.exponential_succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential (x + 1) y ↔ ∃ (z : V), y = 2 * z ∧ LO.Arith.Exponential x z
theorem
LO.Arith.Exponential.exponential_succ_mul_two
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential (x + 1) (2 * y) ↔ LO.Arith.Exponential x y
theorem
LO.Arith.Exponential.succ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential x y → LO.Arith.Exponential (x + 1) (2 * y)
Alias of the reverse direction of LO.Arith.Exponential.exponential_succ_mul_two
.
theorem
LO.Arith.Exponential.of_succ_two_mul
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
LO.Arith.Exponential (x + 1) (2 * y) → LO.Arith.Exponential x y
Alias of the forward direction of LO.Arith.Exponential.exponential_succ_mul_two
.
theorem
LO.Arith.Exponential.one_le_ext_of_seq₀_of_seqₛ
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
{X : V}
{Y : V}
(h₀ : LO.Arith.Exponential.Seq₀ X Y)
(hₛ : LO.Arith.Exponential.Seqₛ y X Y)
{i : V}
(ne2 : i ≠ 2)
(hi : i ≤ y ^ 2)
(ppi : LO.Arith.PPow2 i)
:
1 ≤ LO.Arith.ext i X
theorem
LO.Arith.Exponential.zero_uniq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
(h : LO.Arith.Exponential 0 y)
:
y = 1
@[simp]
theorem
LO.Arith.Exponential.zero_uniq_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{y : V}
:
LO.Arith.Exponential 0 y ↔ y = 1
theorem
LO.Arith.Exponential.succ_lt_s
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
(h : LO.Arith.Exponential (x + 1) y)
:
2 ≤ y
theorem
LO.Arith.Exponential.uniq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y₁ : V}
{y₂ : V}
:
LO.Arith.Exponential x y₁ → LO.Arith.Exponential x y₂ → y₁ = y₂
theorem
LO.Arith.Exponential.inj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x₁ : V}
{x₂ : V}
{y : V}
:
LO.Arith.Exponential x₁ y → LO.Arith.Exponential x₂ y → x₁ = x₂
theorem
LO.Arith.Exponential.exponential_elim
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x : V}
{y : V}
:
theorem
LO.Arith.Exponential.monotone
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x₁ : V}
{x₂ : V}
{y₁ : V}
{y₂ : V}
:
LO.Arith.Exponential x₁ y₁ → LO.Arith.Exponential x₂ y₂ → x₁ < x₂ → y₁ < y₂
theorem
LO.Arith.Exponential.monotone_le
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x₁ : V}
{x₂ : V}
{y₁ : V}
{y₂ : V}
(h₁ : LO.Arith.Exponential x₁ y₁)
(h₂ : LO.Arith.Exponential x₂ y₂)
:
theorem
LO.Arith.Exponential.monotone_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x₁ : V}
{x₂ : V}
{y₁ : V}
{y₂ : V}
(h₁ : LO.Arith.Exponential x₁ y₁)
(h₂ : LO.Arith.Exponential x₂ y₂)
:
theorem
LO.Arith.Exponential.monotone_le_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x₁ : V}
{x₂ : V}
{y₁ : V}
{y₂ : V}
(h₁ : LO.Arith.Exponential x₁ y₁)
(h₂ : LO.Arith.Exponential x₂ y₂)
:
theorem
LO.Arith.Exponential.add_mul
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₀]
{x₁ : V}
{x₂ : V}
{y₁ : V}
{y₂ : V}
(h₁ : LO.Arith.Exponential x₁ y₁)
(h₂ : LO.Arith.Exponential x₂ y₂)
:
LO.Arith.Exponential (x₁ + x₂) (y₁ * y₂)
theorem
LO.Arith.Exponential.range_exists
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
:
∃ (y : V), LO.Arith.Exponential x y
theorem
LO.Arith.Exponential.range_exists_unique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(x : V)
:
∃! y : V, LO.Arith.Exponential x y
Equations
- LO.Arith.instExp_arithmetization = { exp := fun (a : V) => Classical.choose! ⋯ }
theorem
LO.Arith.exponential_exp
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(a : V)
:
LO.Arith.Exponential a (exp a)
theorem
LO.Arith.exponential_graph
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{a : V}
{b : V}
:
a = exp b ↔ LO.Arith.Exponential b a
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
instance
LO.Arith.exp_definable_deltaZero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ exp
Equations
- ⋯ = ⋯
theorem
LO.Arith.exp_of_exponential
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{a : V}
{b : V}
(h : LO.Arith.Exponential a b)
:
@[simp]
@[simp]
@[simp]
@[simp]
theorem
LO.Arith.exp_pow2
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(a : V)
:
LO.Arith.Pow2 (exp a)