Beginning of Section SurrealMinus
Primitive. The name
minus_SNo is a term of type
set → set.
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 490 and no associativity corresponding to applying term
SNoLe.
Axiom. (
minus_SNo_eq) We take the following as an axiom:
∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Axiom. (
minus_SNo_prop1) We take the following as an axiom:
∀x, SNo x → SNo (- x) ∧ (∀u ∈ SNoL x, - x < - u) ∧ (∀u ∈ SNoR x, - u < - x) ∧ SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Axiom. (
minus_SNo_SNoCutP) We take the following as an axiom:
∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
Axiom. (
minus_SNo_SNoCutP_gen) We take the following as an axiom:
∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}
Axiom. (
minus_SNo_Lev_lem1) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, SNoLev (- x) ⊆ SNoLev x
Axiom. (
minus_SNo_Lev) We take the following as an axiom:
∀x, SNo x → SNoLev (- x) = SNoLev x
Axiom. (
minus_SNo_SNo_) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNo_ alpha (- x)
Axiom. (
minus_SNo_SNoS_) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, x ∈ SNoS_ alpha → - x ∈ SNoS_ alpha
Axiom. (
minus_SNoCut_eq_lem) We take the following as an axiom:
∀v, SNo v → ∀L R, SNoCutP L R → v = SNoCut L R → - v = SNoCut {- z|z ∈ R} {- w|w ∈ L}
Axiom. (
minus_SNoCut_eq) We take the following as an axiom:
∀L R, SNoCutP L R → - SNoCut L R = SNoCut {- z|z ∈ R} {- w|w ∈ L}
Axiom. (
mordinal_SNoLev_min_2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → - alpha ≤ z
Axiom. (
SNoL_minus_SNoR) We take the following as an axiom:
∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}
End of Section SurrealMinus