Beginning of Section SurrealMinus
(*** $I sig/Part1.mgs ***)
(*** $I sig/Part2.mgs ***)
(*** $I sig/Part3.mgs ***)
(*** Part 4 ***)
L9
Definition. We define minus_SNo to be SNo_rec_i (λx m ⇒ SNoCut {m z|z ∈ SNoR x} {m w|w ∈ SNoL x}) of type set → set.
In Proofgold the corresponding term root is 268a6c... and object id is 8a6d85...
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.
L16
Theorem. (minus_SNo_eq)
∀x, SNo x → - x = SNoCut {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
In Proofgold the corresponding term root is c9793e... and proposition id is 570cba...
Proof:
Proof not loaded.
L47
Theorem. (minus_SNo_prop1)
∀x, SNo x → SNo (- x) ∧ (∀u ∈ SNoL x, - x < - u) ∧ (∀u ∈ SNoR x, - u < - x) ∧ SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
In Proofgold the corresponding term root is 7c0e82... and proposition id is f0b75f...
Proof:
Proof not loaded.
L238
Theorem. (SNo_minus_SNo)
∀x, SNo x → SNo (- x)
In Proofgold the corresponding term root is 5cf7d9... and proposition id is 744cc2...
Proof:
Proof not loaded.
L245
Theorem. (minus_SNo_Lt_contra)
∀x y, SNo x → SNo y → x < y → - y < - x
In Proofgold the corresponding term root is 5ce52d... and proposition id is 3ebf6e...
Proof:
Proof not loaded.
L314
Theorem. (minus_SNo_Le_contra)
∀x y, SNo x → SNo y → x ≤ y → - y ≤ - x
In Proofgold the corresponding term root is c1b225... and proposition id is f8c896...
Proof:
Proof not loaded.
L332
Theorem. (minus_SNo_SNoCutP)
∀x, SNo x → SNoCutP {- z|z ∈ SNoR x} {- w|w ∈ SNoL x}
In Proofgold the corresponding term root is 99c6fc... and proposition id is 5ad5e4...
Proof:
Proof not loaded.
L340
Theorem. (minus_SNo_SNoCutP_gen)
∀L R, SNoCutP L R → SNoCutP {- z|z ∈ R} {- w|w ∈ L}
In Proofgold the corresponding term root is e7650d... and proposition id is 687fea...
Proof:
Proof not loaded.
L391
Theorem. (minus_SNo_Lev_lem1)
∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, SNoLev (- x) ⊆ SNoLev x
In Proofgold the corresponding term root is 14986a... and proposition id is afc115...
Proof:
Proof not loaded.
L562
Theorem. (minus_SNo_Lev_lem2)
∀x, SNo x → SNoLev (- x) ⊆ SNoLev x
In Proofgold the corresponding term root is 879020... and proposition id is 19cf80...
Proof:
Proof not loaded.
L573
Theorem. (minus_SNo_invol)
∀x, SNo x → - - x = x
In Proofgold the corresponding term root is 44bfe8... and proposition id is cc64ee...
Proof:
Proof not loaded.
L641
Theorem. (minus_SNo_Lev)
∀x, SNo x → SNoLev (- x) = SNoLev x
In Proofgold the corresponding term root is f65499... and proposition id is 476ae5...
Proof:
Proof not loaded.
L652
Theorem. (minus_SNo_SNo_)
∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNo_ alpha (- x)
In Proofgold the corresponding term root is 84605f... and proposition id is 14bd6d...
Proof:
Proof not loaded.
L669
Theorem. (minus_SNo_SNoS_)
∀alpha, ordinal alpha → ∀x, x ∈ SNoS_ alpha → - x ∈ SNoS_ alpha
In Proofgold the corresponding term root is 12f1a5... and proposition id is e10c92...
Proof:
Proof not loaded.
L682
Theorem. (minus_SNoCut_eq_lem)
∀v, SNo v → ∀L R, SNoCutP L R → v = SNoCut L R → - v = SNoCut {- z|z ∈ R} {- w|w ∈ L}
In Proofgold the corresponding term root is 29069a... and proposition id is 11eb03...
Proof:
Proof not loaded.
L792
Theorem. (minus_SNoCut_eq)
∀L R, SNoCutP L R → - SNoCut L R = SNoCut {- z|z ∈ R} {- w|w ∈ L}
In Proofgold the corresponding term root is 083ffe... and proposition id is 54736f...
Proof:
Proof not loaded.
L797
Theorem. (minus_SNo_Lt_contra1)
∀x y, SNo x → SNo y → - x < y → - y < x
In Proofgold the corresponding term root is 226757... and proposition id is 298729...
Proof:
Proof not loaded.
L810
Theorem. (minus_SNo_Lt_contra2)
∀x y, SNo x → SNo y → x < - y → y < - x
In Proofgold the corresponding term root is c6f2da... and proposition id is f41968...
Proof:
Proof not loaded.
L823
Theorem. (mordinal_SNoLev_min_2)
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → - alpha ≤ z
In Proofgold the corresponding term root is 2766c7... and proposition id is a96d68...
Proof:
Proof not loaded.
L839
Theorem. (minus_SNo_SNoS_omega)
∀x ∈ SNoS_ ω, - x ∈ SNoS_ ω
In Proofgold the corresponding term root is daeba5... and proposition id is 0c19f5...
Proof:
Proof not loaded.
L855
Theorem. (SNoL_minus_SNoR)
∀x, SNo x → SNoL (- x) = {- w|w ∈ SNoR x}
In Proofgold the corresponding term root is 084b2d... and proposition id is 8b2b92...
Proof:
Proof not loaded.
End of Section SurrealMinus