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.
L10Axiom. (
minus_SNo_eq) We take the following as an axiom:
∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
L11Axiom. (
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}
L15Axiom. (
minus_SNo_SNoCutP) We take the following as an axiom:
∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
L16Axiom. (
minus_SNo_SNoCutP_gen) We take the following as an axiom:
∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}
L17Axiom. (
minus_SNo_Lev_lem1) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, SNoLev (- x) ⊆ SNoLev x
L20Axiom. (
minus_SNo_Lev) We take the following as an axiom:
∀x, SNo x → SNoLev (- x) = SNoLev x
L21Axiom. (
minus_SNo_SNo_) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNo_ alpha (- x)
L22Axiom. (
minus_SNo_SNoS_) We take the following as an axiom:
∀alpha, ordinal alpha → ∀x, x ∈ SNoS_ alpha → - x ∈ SNoS_ alpha
L23Axiom. (
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}
L24Axiom. (
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}
L27Axiom. (
mordinal_SNoLev_min_2) We take the following as an axiom:
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → - alpha ≤ z
L29Axiom. (
SNoL_minus_SNoR) We take the following as an axiom:
∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}
End of Section SurrealMinus