Beginning of Section Int
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo.
Primitive. The name
int is a term of type
set.
Axiom. (
int_SNo_cases) We take the following as an axiom:
∀p : set → prop, (∀n ∈ ω, p n) → (∀n ∈ ω, p (- n)) → ∀x ∈ int, p x
Axiom. (
int_3_cases) We take the following as an axiom:
∀n ∈ int, ∀p : prop, (∀m ∈ ω, n = - ordsucc m → p) → (n = 0 → p) → (∀m ∈ ω, n = ordsucc m → p) → p
Axiom. (
int_SNo) We take the following as an axiom:
Axiom. (
int_add_SNo) We take the following as an axiom:
Axiom. (
int_mul_SNo) We take the following as an axiom:
End of Section Int
Beginning of Section SurrealAbs
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo.
Primitive. The name
abs_SNo is a term of type
set → set.
Axiom. (
abs_SNo_0) We take the following as an axiom:
Axiom. (
pos_abs_SNo) We take the following as an axiom:
Axiom. (
neg_abs_SNo) We take the following as an axiom:
Axiom. (
SNo_abs_SNo) We take the following as an axiom:
Axiom. (
abs_SNo_Lev) We take the following as an axiom:
∀x, SNo x → SNoLev (abs_SNo x) = SNoLev x
End of Section SurrealAbs
Beginning of Section SNoMaxMin
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo.
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat.
Notation. We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt.
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe.
Definition. We define
SNo_max_of to be
λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → y ≤ x of type
set → set → prop.
Definition. We define
SNo_min_of to be
λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X, SNo y → x ≤ y of type
set → set → prop.
Axiom. (
double_SNo_max_1) We take the following as an axiom:
∀x y, SNo x → SNo_max_of (SNoL x) y → ∀z, SNo z → x < z → y + z < x + x → ∃w ∈ SNoR z, y + w = x + x
Axiom. (
double_SNo_min_1) We take the following as an axiom:
∀x y, SNo x → SNo_min_of (SNoR x) y → ∀z, SNo z → z < x → x + x < y + z → ∃w ∈ SNoL z, y + w = x + x
End of Section SNoMaxMin
Beginning of Section DiadicRationals
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_SNo.
Notation. We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt.
Notation. We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe.
Notation. We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat.
End of Section DiadicRationals