Primitive . The name
Eps_i is a term of type
(set → prop ) → set .
L2 Axiom. (
Eps_i_ax ) We take the following as an axiom:
∀P : set → prop , ∀x : set , P x → P (Eps_i P )
L3 Definition. We define
True to be
∀p : prop , p → p of type
prop .
L4 Definition. We define
False to be
∀p : prop , p of type
prop .
L5 Definition. We define
not to be
λA : prop ⇒ A → False of type
prop → prop .
Notation . We use
¬ as a prefix operator with priority 700 corresponding to applying term
not .
L8 Definition. We define
and to be
λA B : prop ⇒ ∀p : prop , (A → B → p ) → p of type
prop → prop → prop .
Notation . We use
∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term
and .
L11 Definition. We define
or to be
λA B : prop ⇒ ∀p : prop , (A → p ) → (B → p ) → p of type
prop → prop → prop .
Notation . We use
∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term
or .
L14 Definition. We define
iff to be
λA B : prop ⇒ and (A → B ) (B → A ) of type
prop → prop → prop .
Notation . We use
↔ as an infix operator with priority 805 and no associativity corresponding to applying term
iff .
Beginning of Section Eq
L19 Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop , Q x y → Q y x of type
A → A → prop .
L20 Definition. We define
neq to be
λx y : A ⇒ ¬ eq x y of type
A → A → prop .
End of Section Eq
Notation . We use
= as an infix operator with priority 502 and no associativity corresponding to applying term
eq .
Notation . We use
≠ as an infix operator with priority 502 and no associativity corresponding to applying term
neq .
Beginning of Section FE
L27 Axiom. (
func_ext ) We take the following as an axiom:
∀f g : A → B , (∀x : A , f x = g x ) → f = g
End of Section FE
Beginning of Section Ex
L31 Definition. We define
ex to be
λQ : A → prop ⇒ ∀P : prop , (∀x : A , Q x → P ) → P of type
(A → prop ) → prop .
End of Section Ex
Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex .
L35 Axiom. (
prop_ext ) We take the following as an axiom:
∀p q : prop , iff p q → p = q
Primitive . The name
In is a term of type
set → set → prop .
Notation . We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In . Furthermore, we may write
∀ x ∈ A , B to mean
∀ x : set, x ∈ A → B .
L37 Definition. We define
Subq to be
λA B ⇒ ∀x ∈ A , x ∈ B of type
set → set → prop .
Notation . We use
⊆ as an infix operator with priority 500 and no associativity corresponding to applying term
Subq . Furthermore, we may write
∀ x ⊆ A , B to mean
∀ x : set, x ⊆ A → B .
L38 Axiom. (
set_ext ) We take the following as an axiom:
∀X Y : set , X ⊆ Y → Y ⊆ X → X = Y
L39 Axiom. (
In_ind ) We take the following as an axiom:
∀P : set → prop , (∀X : set , (∀x ∈ X , P x ) → P X ) → ∀X : set , P X
Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex and handling ∈ or ⊆ ascriptions using
and .
Primitive . The name
Empty is a term of type
set .
L42 Axiom. (
EmptyAx ) We take the following as an axiom:
Primitive . The name
⋃ is a term of type
set → set .
L45 Axiom. (
UnionEq ) We take the following as an axiom:
∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X
Primitive . The name
𝒫 is a term of type
set → set .
L48 Axiom. (
PowerEq ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X ↔ Y ⊆ X
Primitive . The name
Repl is a term of type
set → (set → set ) → set .
Notation .
{B | x ∈ A } is notation for
Repl A (λ x . B ).
L51 Axiom. (
ReplEq ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀y : set , y ∈ { F x | x ∈ A } ↔ ∃x ∈ A , y = F x
L52 Definition. We define
TransSet to be
λU : set ⇒ ∀x ∈ U , x ⊆ U of type
set → prop .
L53 Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set , X ∈ U → ⋃ X ∈ U of type
set → prop .
L54 Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set , X ∈ U → 𝒫 X ∈ U of type
set → prop .
L55 Definition. We define
Repl_closed to be
λU : set ⇒ ∀X : set , X ∈ U → ∀F : set → set , (∀x : set , x ∈ X → F x ∈ U ) → { F x | x ∈ X } ∈ U of type
set → prop .
Primitive . The name
UnivOf is a term of type
set → set .
L62 Axiom. (
UnivOf_In ) We take the following as an axiom:
L65 Axiom. (
UnivOf_Min ) We take the following as an axiom:
L69 Theorem. (
andI )
∀A B : prop , A → B → A ∧ B
Proof: Load proof Proof not loaded.
L73
Proof: Load proof Proof not loaded.
L77
Proof: Load proof Proof not loaded.
L81 Theorem. (
iffI )
∀A B : prop , (A → B ) → (B → A ) → (A ↔ B )
Proof: Load proof Proof not loaded.
L85 Theorem. (
pred_ext )
∀P Q : set → prop , (∀x, P x ↔ Q x ) → P = Q
Proof: Load proof Proof not loaded.
L91 Definition. We define
nIn to be
λx X ⇒ ¬ In x X of type
set → set → prop .
Notation . We use
∉ as an infix operator with priority 502 and no associativity corresponding to applying term
nIn .
L96
Proof: Load proof Proof not loaded.
L102 Theorem. (
PowerI )
∀X Y : set , Y ⊆ X → Y ∈ 𝒫 X
Proof: Load proof Proof not loaded.
L106
Proof: Load proof Proof not loaded.
L110
Proof: Load proof Proof not loaded.
L114
Proof: Load proof Proof not loaded.
L165
Proof: Load proof Proof not loaded.
L169
Proof: Load proof Proof not loaded.
L173
Proof: Load proof Proof not loaded.
Beginning of Section PropN
L179 Variable P1 P2 P3 : prop
L180 Theorem. (
and3I )
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
Proof: Load proof Proof not loaded.
L184 Theorem. (
and3E )
P1 ∧ P2 ∧ P3 → (∀p : prop , (P1 → P2 → P3 → p ) → p )
Proof: Load proof Proof not loaded.
L188
Proof: Load proof Proof not loaded.
L192
Proof: Load proof Proof not loaded.
L196
Proof: Load proof Proof not loaded.
L200 Theorem. (
or3E )
P1 ∨ P2 ∨ P3 → (∀p : prop , (P1 → p ) → (P2 → p ) → (P3 → p ) → p )
Proof: Load proof Proof not loaded.
L206 Theorem. (
and4I )
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
Proof: Load proof Proof not loaded.
L212 Theorem. (
and5I )
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
Proof: Load proof Proof not loaded.
L218 Theorem. (
and6I )
P1 → P2 → P3 → P4 → P5 → P6 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6
Proof: Load proof Proof not loaded.
L224 Theorem. (
and7I )
P1 → P2 → P3 → P4 → P5 → P6 → P7 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 ∧ P7
Proof: Load proof Proof not loaded.
End of Section PropN
L230
Proof: Load proof Proof not loaded.
L238
Proof: Load proof Proof not loaded.
L244 Theorem. (
iffEL )
∀A B : prop , (A ↔ B ) → A → B
Proof: Load proof Proof not loaded.
L248 Theorem. (
iffER )
∀A B : prop , (A ↔ B ) → B → A
Proof: Load proof Proof not loaded.
L252
Proof: Load proof Proof not loaded.
L256 Theorem. (
iff_sym )
∀A B : prop , (A ↔ B ) → (B ↔ A )
Proof: Load proof Proof not loaded.
L265 Theorem. (
iff_trans )
∀A B C : prop , (A ↔ B ) → (B ↔ C ) → (A ↔ C )
Proof: Load proof Proof not loaded.
L278
Proof: Load proof Proof not loaded.
L282
Proof: Load proof Proof not loaded.
L286
Proof: Load proof Proof not loaded.
L292 Theorem. (
prop_ext_2 )
∀p q : prop , (p → q ) → (q → p ) → p = q
Proof: Load proof Proof not loaded.
L298
Proof: Load proof Proof not loaded.
L302 Theorem. (
Subq_tra )
∀X Y Z : set , X ⊆ Y → Y ⊆ Z → X ⊆ Z
Proof: Load proof Proof not loaded.
L306
Proof: Load proof Proof not loaded.
L314
Proof: Load proof Proof not loaded.
L324 Theorem. (
UnionI )
∀X x Y : set , x ∈ Y → Y ∈ X → x ∈ ⋃ X
Proof: Load proof Proof not loaded.
L337 Theorem. (
UnionE )
∀X x : set , x ∈ ⋃ X → ∃Y : set , x ∈ Y ∧ Y ∈ X
Proof: Load proof Proof not loaded.
L341 Theorem. (
UnionE_impred )
∀X x : set , x ∈ ⋃ X → ∀p : prop , (∀Y : set , x ∈ Y → Y ∈ X → p ) → p
Proof: Load proof Proof not loaded.
L349 Theorem. (
PowerE )
∀X Y : set , Y ∈ 𝒫 X → Y ⊆ X
Proof: Load proof Proof not loaded.
L353
Proof: Load proof Proof not loaded.
L357
Proof: Load proof Proof not loaded.
L366
Proof: Load proof Proof not loaded.
L376
Proof: Load proof Proof not loaded.
L393 Definition. We define
exactly1of2 to be
λA B : prop ⇒ A ∧ ¬ B ∨ ¬ A ∧ B of type
prop → prop → prop .
L395
Proof: Load proof Proof not loaded.
L405
Proof: Load proof Proof not loaded.
L415
Proof: Load proof Proof not loaded.
L430
Proof: Load proof Proof not loaded.
L438 Theorem. (
ReplI )
∀A : set , ∀F : set → set , ∀x : set , x ∈ A → F x ∈ { F x | x ∈ A }
Proof: Load proof Proof not loaded.
L448 Theorem. (
ReplE )
∀A : set , ∀F : set → set , ∀y : set , y ∈ { F x | x ∈ A } → ∃x ∈ A , y = F x
Proof: Load proof Proof not loaded.
L452 Theorem. (
ReplE_impred )
∀A : set , ∀F : set → set , ∀y : set , y ∈ { F x | x ∈ A } → ∀p : prop , (∀x : set , x ∈ A → y = F x → p ) → p
Proof: Load proof Proof not loaded.
L461 Theorem. (
ReplE' )
∀X, ∀f : set → set , ∀p : set → prop , (∀x ∈ X , p (f x ) ) → ∀y ∈ { f x | x ∈ X } , p y
Proof: Load proof Proof not loaded.
L468
Proof: Load proof Proof not loaded.
L479
Proof: Load proof Proof not loaded.
L494
Proof: Load proof Proof not loaded.
L503 Theorem. (
Repl_inv_eq )
∀P : set → prop , ∀f g : set → set , (∀x, P x → g (f x ) = x ) → ∀X, (∀x ∈ X , P x ) → { g y | y ∈ { f x | x ∈ X } } = X
Proof: Load proof Proof not loaded.
L527 Theorem. (
Repl_invol_eq )
∀P : set → prop , ∀f : set → set , (∀x, P x → f (f x ) = x ) → ∀X, (∀x ∈ X , P x ) → { f y | y ∈ { f x | x ∈ X } } = X
Proof: Load proof Proof not loaded.
L536 Definition. We define
If_i to be
(λp x y ⇒ Eps_i (λz : set ⇒ p ∧ z = x ∨ ¬ p ∧ z = y ) ) of type
prop → set → set → set .
Notation .
if cond then T else E is notation corresponding to
If_i type cond T E where
type is the inferred type of
T .
L538
Proof: Load proof Proof not loaded.
L560
Proof: Load proof Proof not loaded.
L571
Proof: Load proof Proof not loaded.
L582
Proof: Load proof Proof not loaded.
Notation .
{x ,y } is notation for
UPair x y .
L594
Proof: Load proof Proof not loaded.
L614
Proof: Load proof Proof not loaded.
L625
Proof: Load proof Proof not loaded.
L638 Definition. We define
Sing to be
λx ⇒ { x , x } of type
set → set .
Notation .
{x } is notation for
Sing x .
L640
Proof: Load proof Proof not loaded.
L644
Proof: Load proof Proof not loaded.
L650 Definition. We define
binunion to be
λX Y ⇒ ⋃ { X , Y } of type
set → set → set .
Notation . We use
∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term
binunion .
L653
Proof: Load proof Proof not loaded.
L663
Proof: Load proof Proof not loaded.
L673
Proof: Load proof Proof not loaded.
L696 Theorem. (
binunionE' )
∀X Y z, ∀p : prop , (z ∈ X → p ) → (z ∈ Y → p ) → (z ∈ X ∪ Y → p )
Proof: Load proof Proof not loaded.
L703
Proof: Load proof Proof not loaded.
L729
Proof: Load proof Proof not loaded.
L737
Proof: Load proof Proof not loaded.
L743
Proof: Load proof Proof not loaded.
L752
Proof: Load proof Proof not loaded.
L758
Proof: Load proof Proof not loaded.
L762
Proof: Load proof Proof not loaded.
L766
Proof: Load proof Proof not loaded.
L777
Proof: Load proof Proof not loaded.
L793 Definition. We define
SetAdjoin to be
λX y ⇒ X ∪ { y } of type
set → set → set .
Notation . We now use the set enumeration notation
{...,...,...} in general. If 0 elements are given, then
Empty is used to form the corresponding term. If 1 element is given, then
Sing is used to form the corresponding term. If 2 elements are given, then
UPair is used to form the corresponding term. If more than elements are given, then
SetAdjoin is used to reduce to the case with one fewer elements.
L797 Definition. We define
famunion to be
λX F ⇒ ⋃ { F x | x ∈ X } of type
set → (set → set ) → set .
Notation . We use
⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
famunion .
L802 Theorem. (
famunionI )
∀X : set , ∀F : (set → set ) , ∀x y : set , x ∈ X → y ∈ F x → y ∈ ⋃ x ∈ X F x
Proof: Load proof Proof not loaded.
L806 Theorem. (
famunionE )
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃ x ∈ X F x ) → ∃x ∈ X , y ∈ F x
Proof: Load proof Proof not loaded.
L827 Theorem. (
famunionE_impred )
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃ x ∈ X F x ) → ∀p : prop , (∀x, x ∈ X → y ∈ F x → p ) → p
Proof: Load proof Proof not loaded.
L835
Proof: Load proof Proof not loaded.
L842
Proof: Load proof Proof not loaded.
L852
Proof: Load proof Proof not loaded.
Beginning of Section SepSec
L864 Variable P : set → prop
L865 Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z )
End of Section SepSec
Notation .
{x ∈ A | B } is notation for
Sep A (λ x . B ).
L872 Theorem. (
SepI )
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ X → P x → x ∈ { x ∈ X | P x }
Proof: Load proof Proof not loaded.
L910 Theorem. (
SepE )
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ { x ∈ X | P x } → x ∈ X ∧ P x
Proof: Load proof Proof not loaded.
L961 Theorem. (
SepE1 )
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ { x ∈ X | P x } → x ∈ X
Proof: Load proof Proof not loaded.
L965 Theorem. (
SepE2 )
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ { x ∈ X | P x } → P x
Proof: Load proof Proof not loaded.
L969
Proof: Load proof Proof not loaded.
L975
Proof: Load proof Proof not loaded.
L979
Proof: Load proof Proof not loaded.
L985 Definition. We define
ReplSep to be
λX P F ⇒ { F x | x ∈ { z ∈ X | P z } } of type
set → (set → prop ) → (set → set ) → set .
Notation .
{B | x ∈ A , C } is notation for
ReplSep A (λ x . C ) (λ x . B ).
L987 Theorem. (
ReplSepI )
∀X : set , ∀P : set → prop , ∀F : set → set , ∀x : set , x ∈ X → P x → F x ∈ { F x | x ∈ X , P x }
Proof: Load proof Proof not loaded.
L991 Theorem. (
ReplSepE )
∀X : set , ∀P : set → prop , ∀F : set → set , ∀y : set , y ∈ { F x | x ∈ X , P x } → ∃x : set , x ∈ X ∧ P x ∧ y = F x
Proof: Load proof Proof not loaded.
L1010 Theorem. (
ReplSepE_impred )
∀X : set , ∀P : set → prop , ∀F : set → set , ∀y : set , y ∈ { F x | x ∈ X , P x } → ∀p : prop , (∀x ∈ X , P x → y = F x → p ) → p
Proof: Load proof Proof not loaded.
L1023 Definition. We define
binintersect to be
λX Y ⇒ { x ∈ X | x ∈ Y } of type
set → set → set .
Notation . We use
∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term
binintersect .
L1027
Proof: Load proof Proof not loaded.
L1031
Proof: Load proof Proof not loaded.
L1035
Proof: Load proof Proof not loaded.
L1039
Proof: Load proof Proof not loaded.
L1043
Proof: Load proof Proof not loaded.
L1047
Proof: Load proof Proof not loaded.
L1051
Proof: Load proof Proof not loaded.
L1062
Proof: Load proof Proof not loaded.
L1073
Proof: Load proof Proof not loaded.
L1079
Proof: Load proof Proof not loaded.
L1087 Definition. We define
setminus to be
λX Y ⇒ Sep X (λx ⇒ x ∉ Y ) of type
set → set → set .
Notation . We use
∖ as an infix operator with priority 350 and no associativity corresponding to applying term
setminus .
L1091
Proof: Load proof Proof not loaded.
L1095
Proof: Load proof Proof not loaded.
L1099
Proof: Load proof Proof not loaded.
L1103
Proof: Load proof Proof not loaded.
L1107
Proof: Load proof Proof not loaded.
L1111
Proof: Load proof Proof not loaded.
L1115
Proof: Load proof Proof not loaded.
L1140
Proof: Load proof Proof not loaded.
L1149
Proof: Load proof Proof not loaded.
L1161 Definition. We define
ordsucc to be
λx : set ⇒ x ∪ { x } of type
set → set .
L1162
Proof: Load proof Proof not loaded.
L1167
Proof: Load proof Proof not loaded.
L1171
Proof: Load proof Proof not loaded.
Notation . Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc .
L1181
Proof: Load proof Proof not loaded.
L1189
Proof: Load proof Proof not loaded.
L1193
Proof: Load proof Proof not loaded.
L1214
Proof: Load proof Proof not loaded.
L1218
Proof: Load proof Proof not loaded.
L1222
Proof: Load proof Proof not loaded.
L1226 Definition. We define
nat_p to be
λn : set ⇒ ∀p : set → prop , p 0 → (∀x : set , p x → p (ordsucc x ) ) → p n of type
set → prop .
L1228
Proof: Load proof Proof not loaded.
L1232
Proof: Load proof Proof not loaded.
L1236
Proof: Load proof Proof not loaded.
L1240
Proof: Load proof Proof not loaded.
L1244
Proof: Load proof Proof not loaded.
L1256
Proof: Load proof Proof not loaded.
L1282
Proof: Load proof Proof not loaded.
L1307
Proof: Load proof Proof not loaded.
L1337
Proof: Load proof Proof not loaded.
L1341
Proof: Load proof Proof not loaded.
L1349
Proof: Load proof Proof not loaded.
L1370
Proof: Load proof Proof not loaded.
L1396
Proof: Load proof Proof not loaded.
L1412 Definition. We define
surj to be
λX Y f ⇒ (∀u ∈ X , f u ∈ Y ) ∧ (∀w ∈ Y , ∃u ∈ X , f u = w ) of type
set → set → (set → set ) → prop .
L1418
Proof: Load proof Proof not loaded.
L1444 Definition. We define
inj to be
λX Y f ⇒ (∀u ∈ X , f u ∈ Y ) ∧ (∀u v ∈ X , f u = f v → u = v ) of type
set → set → (set → set ) → prop .
L1450
Proof: Load proof Proof not loaded.
L1481 Theorem. (
injI )
∀X Y, ∀f : set → set , (∀x ∈ X , f x ∈ Y ) → (∀x z ∈ X , f x = f z → x = z ) → inj X Y f
Proof: Load proof Proof not loaded.
L1489 Theorem. (
inj_comp )
∀X Y Z : set , ∀f g : set → set , inj X Y f → inj Y Z g → inj X Z (λx ⇒ g (f x ) )
Proof: Load proof Proof not loaded.
L1509 Definition. We define
bij to be
λX Y f ⇒ (∀u ∈ X , f u ∈ Y ) ∧ (∀u v ∈ X , f u = f v → u = v ) ∧ (∀w ∈ Y , ∃u ∈ X , f u = w ) of type
set → set → (set → set ) → prop .
L1517 Theorem. (
bijI )
∀X Y, ∀f : set → set , (∀u ∈ X , f u ∈ Y ) → (∀u v ∈ X , f u = f v → u = v ) → (∀w ∈ Y , ∃u ∈ X , f u = w ) → bij X Y f
Proof: Load proof Proof not loaded.
L1532 Theorem. (
bijE )
∀X Y, ∀f : set → set , bij X Y f → ∀p : prop , ((∀u ∈ X , f u ∈ Y ) → (∀u v ∈ X , f u = f v → u = v ) → (∀w ∈ Y , ∃u ∈ X , f u = w ) → p ) → p
Proof: Load proof Proof not loaded.
L1546
Proof: Load proof Proof not loaded.
L1550
Proof: Load proof Proof not loaded.
L1561 Theorem. (
bij_comp )
∀X Y Z : set , ∀f g : set → set , bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x ) )
Proof: Load proof Proof not loaded.
L1593
Proof: Load proof Proof not loaded.
L1603 Definition. We define
inv to be
λX f ⇒ λy : set ⇒ Eps_i (λx ⇒ x ∈ X ∧ f x = y ) of type
set → (set → set ) → set → set .
L1605 Theorem. (
surj_rinv )
∀X Y, ∀f : set → set , (∀w ∈ Y , ∃u ∈ X , f u = w ) → ∀y ∈ Y , inv X f y ∈ X ∧ f (inv X f y ) = y
Proof: Load proof Proof not loaded.
L1614 Theorem. (
inj_linv )
∀X, ∀f : set → set , (∀u v ∈ X , f u = f v → u = v ) → ∀x ∈ X , inv X f (f x ) = x
Proof: Load proof Proof not loaded.
L1629
Proof: Load proof Proof not loaded.
L1670 Definition. We define
atleastp to be
λX Y : set ⇒ ∃f : set → set , inj X Y f of type
set → set → prop .
L1673
Proof: Load proof Proof not loaded.
L1687
Proof: Load proof Proof not loaded.
L1700 Definition. We define
equip to be
λX Y : set ⇒ ∃f : set → set , bij X Y f of type
set → set → prop .
L1703
Proof: Load proof Proof not loaded.
L1713
Proof: Load proof Proof not loaded.
L1720
Proof: Load proof Proof not loaded.
L1729
Proof: Load proof Proof not loaded.
L1740
Proof: Load proof Proof not loaded.
L1753
Proof: Load proof Proof not loaded.
L1843
Proof: Load proof Proof not loaded.
Beginning of Section SchroederBernstein
L2039
Proof: Load proof Proof not loaded.
L2080
Proof: Load proof Proof not loaded.
L2093
Proof: Load proof Proof not loaded.
L2104
Proof: Load proof Proof not loaded.
L2112
Proof: Load proof Proof not loaded.
L2266
Proof: Load proof Proof not loaded.
End of Section SchroederBernstein
Beginning of Section PigeonHole
L2281
Proof: Load proof Proof not loaded.
L2428
Proof: Load proof Proof not loaded.
End of Section PigeonHole
L2440
Proof: Load proof Proof not loaded.
L2463 Theorem. (
cases_1 )
∀i ∈ 1 , ∀p : set → prop , p 0 → p i
Proof: Load proof Proof not loaded.
L2472 Theorem. (
cases_2 )
∀i ∈ 2 , ∀p : set → prop , p 0 → p 1 → p i
Proof: Load proof Proof not loaded.
L2481
Proof: Load proof Proof not loaded.
L2485
Proof: Load proof Proof not loaded.
L2489
Proof: Load proof Proof not loaded.
L2493
Proof: Load proof Proof not loaded.
L2499
Proof: Load proof Proof not loaded.
L2503
Proof: Load proof Proof not loaded.
L2516
Proof: Load proof Proof not loaded.
L2536
Proof: Load proof Proof not loaded.
L2557
Proof: Load proof Proof not loaded.
L2577
Proof: Load proof Proof not loaded.
L2588
Proof: Load proof Proof not loaded.
L2592
Proof: Load proof Proof not loaded.
L2596
Proof: Load proof Proof not loaded.
L2613
Proof: Load proof Proof not loaded.
L2619
Proof: Load proof Proof not loaded.
L2687
Proof: Load proof Proof not loaded.
L2692
Proof: Load proof Proof not loaded.
L2709
Proof: Load proof Proof not loaded.
L2722
Proof: Load proof Proof not loaded.
L2739
Proof: Load proof Proof not loaded.
L2754
Proof: Load proof Proof not loaded.
L2769
Proof: Load proof Proof not loaded.
L2800
Proof: Load proof Proof not loaded.
L2814
Proof: Load proof Proof not loaded.
L2829 Theorem. (
ordinal_ind )
∀p : set → prop , (∀alpha, ordinal alpha → (∀beta ∈ alpha , p beta ) → p alpha ) → ∀alpha, ordinal alpha → p alpha
Proof: Load proof Proof not loaded.
L2849
Proof: Load proof Proof not loaded.
L2871
Proof: Load proof Proof not loaded.
L2890
Proof: Load proof Proof not loaded.
L2896 Theorem. (
exandE_i )
∀P Q : set → prop , (∃x, P x ∧ Q x ) → ∀r : prop , (∀x, P x → Q x → r ) → r
Proof: Load proof Proof not loaded.
L2901 Theorem. (
exandE_ii )
∀P Q : (set → set ) → prop , (∃x : set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set , P x → Q x → p ) → p
Proof: Load proof Proof not loaded.
L2908 Theorem. (
exandE_iii )
∀P Q : (set → set → set ) → prop , (∃x : set → set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set → set , P x → Q x → p ) → p
Proof: Load proof Proof not loaded.
L2915 Theorem. (
exandE_iiii )
∀P Q : (set → set → set → set ) → prop , (∃x : set → set → set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set → set → set , P x → Q x → p ) → p
Proof: Load proof Proof not loaded.
Beginning of Section Descr_ii
L2924 Variable P : (set → set ) → prop
L2926 Definition. We define
Descr_ii to be
λx : set ⇒ Eps_i (λy ⇒ ∀h : set → set , P h → h x = y ) of type
set → set .
L2927 Hypothesis Pex : ∃f : set → set , P f
L2928 Hypothesis Puniq : ∀f g : set → set , P f → P g → f = g
L2929
Proof: Load proof Proof not loaded.
End of Section Descr_ii
Beginning of Section Descr_iii
L2949 Variable P : (set → set → set ) → prop
L2951 Definition. We define
Descr_iii to be
λx y : set ⇒ Eps_i (λz ⇒ ∀h : set → set → set , P h → h x y = z ) of type
set → set → set .
L2952 Hypothesis Pex : ∃f : set → set → set , P f
L2953 Hypothesis Puniq : ∀f g : set → set → set , P f → P g → f = g
L2954
Proof: Load proof Proof not loaded.
End of Section Descr_iii
Beginning of Section Descr_Vo1
L2978 Definition. We define
Descr_Vo1 to be
λx : set ⇒ ∀h : set → prop , P h → h x of type
Vo 1 .
L2979 Hypothesis Pex : ∃f : Vo 1 , P f
L2980 Hypothesis Puniq : ∀f g : Vo 1 , P f → P g → f = g
L2981
Proof: Load proof Proof not loaded.
End of Section Descr_Vo1
Beginning of Section If_ii
L3001 Variable f g : set → set
L3003 Definition. We define
If_ii to be
λx ⇒ if p then f x else g x of type
set → set .
L3004
Proof: Load proof Proof not loaded.
L3011
Proof: Load proof Proof not loaded.
End of Section If_ii
Beginning of Section If_iii
L3022 Variable f g : set → set → set
L3024 Definition. We define
If_iii to be
λx y ⇒ if p then f x y else g x y of type
set → set → set .
L3025
Proof: Load proof Proof not loaded.
L3035
Proof: Load proof Proof not loaded.
End of Section If_iii
Beginning of Section EpsilonRec_i
L3048 Variable F : set → (set → set ) → set
L3049 Definition. We define
In_rec_i_G to be
λX Y ⇒ ∀R : set → set → prop , (∀X : set , ∀f : set → set , (∀x ∈ X , R x (f x ) ) → R X (F X f ) ) → R X Y of type
set → set → prop .
L3056
Proof: Load proof Proof not loaded.
L3072
Proof: Load proof Proof not loaded.
L3095 Hypothesis Fr : ∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → F X g = F X h
L3097
Proof: Load proof Proof not loaded.
L3128
Proof: Load proof Proof not loaded.
L3139
Proof: Load proof Proof not loaded.
L3147
Proof: Load proof Proof not loaded.
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
L3154 Variable F : set → (set → (set → set ) ) → (set → set )
L3155 Definition. We define
In_rec_G_ii to be
λX Y ⇒ ∀R : set → (set → set ) → prop , (∀X : set , ∀f : set → (set → set ) , (∀x ∈ X , R x (f x ) ) → R X (F X f ) ) → R X Y of type
set → (set → set ) → prop .
L3162
Proof: Load proof Proof not loaded.
L3178
Proof: Load proof Proof not loaded.
L3201 Hypothesis Fr : ∀X : set , ∀g h : set → (set → set ) , (∀x ∈ X , g x = h x ) → F X g = F X h
L3203
Proof: Load proof Proof not loaded.
L3234
Proof: Load proof Proof not loaded.
L3247
Proof: Load proof Proof not loaded.
L3255
Proof: Load proof Proof not loaded.
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
L3262 Variable F : set → (set → (set → set → set ) ) → (set → set → set )
L3263 Definition. We define
In_rec_G_iii to be
λX Y ⇒ ∀R : set → (set → set → set ) → prop , (∀X : set , ∀f : set → (set → set → set ) , (∀x ∈ X , R x (f x ) ) → R X (F X f ) ) → R X Y of type
set → (set → set → set ) → prop .
L3270
Proof: Load proof Proof not loaded.
L3286
Proof: Load proof Proof not loaded.
L3309 Hypothesis Fr : ∀X : set , ∀g h : set → (set → set → set ) , (∀x ∈ X , g x = h x ) → F X g = F X h
L3311
Proof: Load proof Proof not loaded.
L3342
Proof: Load proof Proof not loaded.
L3355
Proof: Load proof Proof not loaded.
L3363
Proof: Load proof Proof not loaded.
End of Section EpsilonRec_iii
Beginning of Section NatRec
L3371 Variable f : set → set → set
L3372 Let F : set → (set → set ) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n ) (g (⋃ n ) ) else z
L3374 Theorem. (
nat_primrec_r )
∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → F X g = F X h
Proof: Load proof Proof not loaded.
L3394
Proof: Load proof Proof not loaded.
L3402
Proof: Load proof Proof not loaded.
End of Section NatRec
Beginning of Section NatAdd
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
L3421
Proof: Load proof Proof not loaded.
L3426
Proof: Load proof Proof not loaded.
L3431
Proof: Load proof Proof not loaded.
L3450
Proof: Load proof Proof not loaded.
L3459
Proof: Load proof Proof not loaded.
L3481
Proof: Load proof Proof not loaded.
L3495
Proof: Load proof Proof not loaded.
L3514
Proof: Load proof Proof not loaded.
L3532
Proof: Load proof Proof not loaded.
L3550
Proof: Load proof Proof not loaded.
L3558
Proof: Load proof Proof not loaded.
L3580
Proof: Load proof Proof not loaded.
L3590
Proof: Load proof Proof not loaded.
L3604
Proof: Load proof Proof not loaded.
L3642
Proof: Load proof Proof not loaded.
End of Section NatAdd
Beginning of Section NatMul
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
L3669 Definition. We define
mul_nat to be
λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r ) m of type
set → set → set .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
L3672
Proof: Load proof Proof not loaded.
L3677
Proof: Load proof Proof not loaded.
L3682
Proof: Load proof Proof not loaded.
L3691
Proof: Load proof Proof not loaded.
L3708
Proof: Load proof Proof not loaded.
L3723
Proof: Load proof Proof not loaded.
L3755
Proof: Load proof Proof not loaded.
L3775
Proof: Load proof Proof not loaded.
L3806
Proof: Load proof Proof not loaded.
L3835
Proof: Load proof Proof not loaded.
L3857
Proof: Load proof Proof not loaded.
L3865
Proof: Load proof Proof not loaded.
L3880
Proof: Load proof Proof not loaded.
L3901
Proof: Load proof Proof not loaded.
L3937
Proof: Load proof Proof not loaded.
L3954 Definition. We define
Pi_nat to be
λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i ) n of type
(set → set ) → set → set .
L3957
Proof: Load proof Proof not loaded.
L3962
Proof: Load proof Proof not loaded.
L3968
Proof: Load proof Proof not loaded.
L3993
Proof: Load proof Proof not loaded.
L4036 Definition. We define
exp_nat to be
λn m : set ⇒ nat_primrec 1 (λ_ r ⇒ n * r ) m of type
set → set → set .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_nat .
L4040
Proof: Load proof Proof not loaded.
L4046
Proof: Load proof Proof not loaded.
L4052
Proof: Load proof Proof not loaded.
L4063
Proof: Load proof Proof not loaded.
End of Section NatMul
Beginning of Section form100_52
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_nat .
L4080
Proof: Load proof Proof not loaded.
L4084
Proof: Load proof Proof not loaded.
L4098
Proof: Load proof Proof not loaded.
L4102
Proof: Load proof Proof not loaded.
L4123
Proof: Load proof Proof not loaded.
End of Section form100_52
L4496
Proof: Load proof Proof not loaded.
L4505
Proof: Load proof Proof not loaded.
L4510
Proof: Load proof Proof not loaded.
L4515
Proof: Load proof Proof not loaded.
L4520
Proof: Load proof Proof not loaded.
L4604
Proof: Load proof Proof not loaded.
L4609
Proof: Load proof Proof not loaded.
L4614
Proof: Load proof Proof not loaded.
L4619
Proof: Load proof Proof not loaded.
L4634
Proof: Load proof Proof not loaded.
L4638
Proof: Load proof Proof not loaded.
L4647
Proof: Load proof Proof not loaded.
L4655
Proof: Load proof Proof not loaded.
L4659
Proof: Load proof Proof not loaded.
L4684
Proof: Load proof Proof not loaded.
L4693
Proof: Load proof Proof not loaded.
L4706
Proof: Load proof Proof not loaded.
L4720
Proof: Load proof Proof not loaded.
L4724 Definition. We define
finite to be
λX ⇒ ∃n ∈ ω , equip X n of type
set → prop .
L4726
Proof: Load proof Proof not loaded.
L4734
Proof: Load proof Proof not loaded.
L4826
Proof: Load proof Proof not loaded.
L4833
Proof: Load proof Proof not loaded.
L4841
Proof: Load proof Proof not loaded.
L4924
Proof: Load proof Proof not loaded.
L4939
Proof: Load proof Proof not loaded.
L4978
Proof: Load proof Proof not loaded.
Beginning of Section InfinitePrimes
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
L5038 Definition. We define
divides_nat to be
λm n ⇒ m ∈ ω ∧ n ∈ ω ∧ ∃k ∈ ω , m * k = n of type
set → set → prop .
L5041
Proof: Load proof Proof not loaded.
L5055
Proof: Load proof Proof not loaded.
L5096
Proof: Load proof Proof not loaded.
L5109
Proof: Load proof Proof not loaded.
L5116
Proof: Load proof Proof not loaded.
L5153
Proof: Load proof Proof not loaded.
L5235
Proof: Load proof Proof not loaded.
L5277
Proof: Load proof Proof not loaded.
L5346
Proof: Load proof Proof not loaded.
End of Section InfinitePrimes
Beginning of Section InfiniteRamsey
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
L5477
Proof: Load proof Proof not loaded.
L5503
Proof: Load proof Proof not loaded.
L5536
Proof: Load proof Proof not loaded.
L5675
Proof: Load proof Proof not loaded.
L5801
Proof: Load proof Proof not loaded.
End of Section InfiniteRamsey
L6652
Proof: Load proof Proof not loaded.
L6669
Proof: Load proof Proof not loaded.
L6677
Proof: Load proof Proof not loaded.
L6686
Proof: Load proof Proof not loaded.
L6701
Proof: Load proof Proof not loaded.
L6711
Proof: Load proof Proof not loaded.
L6717 Definition. We define
Inj0 to be
λX ⇒ { Inj1 x | x ∈ X } of type
set → set .
L6720
Proof: Load proof Proof not loaded.
L6724
Proof: Load proof Proof not loaded.
L6731
Proof: Load proof Proof not loaded.
L6748
Proof: Load proof Proof not loaded.
L6800
Proof: Load proof Proof not loaded.
L6810
Proof: Load proof Proof not loaded.
L6858
Proof: Load proof Proof not loaded.
L6868
Proof: Load proof Proof not loaded.
L6872
Proof: Load proof Proof not loaded.
Notation . We use
+ as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum .
L6892
Proof: Load proof Proof not loaded.
L6902
Proof: Load proof Proof not loaded.
L6912
Proof: Load proof Proof not loaded.
L6924
Proof: Load proof Proof not loaded.
L6957
Proof: Load proof Proof not loaded.
Beginning of Section pair_setsum
L7013
Proof: Load proof Proof not loaded.
L7021
Proof: Load proof Proof not loaded.
L7029 Theorem. (
pairI0 )
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
Proof: Load proof Proof not loaded.
L7034 Theorem. (
pairI1 )
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
Proof: Load proof Proof not loaded.
L7039 Theorem. (
pairE )
∀X Y z, z ∈ pair X Y → (∃x ∈ X , z = pair 0 x ) ∨ (∃y ∈ Y , z = pair 1 y )
Proof: Load proof Proof not loaded.
L7045 Theorem. (
pairE0 )
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
Proof: Load proof Proof not loaded.
L7071 Theorem. (
pairE1 )
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
Proof: Load proof Proof not loaded.
L7099
Proof: Load proof Proof not loaded.
L7114
Proof: Load proof Proof not loaded.
L7138
Proof: Load proof Proof not loaded.
L7153
Proof: Load proof Proof not loaded.
L7177
Proof: Load proof Proof not loaded.
L7197
Proof: Load proof Proof not loaded.
L7219 Definition. We define
Sigma to be
λX Y ⇒ ⋃ x ∈ X { pair x y | y ∈ Y x } of type
set → (set → set ) → set .
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
L7225
Proof: Load proof Proof not loaded.
L7253
Proof: Load proof Proof not loaded.
L7261
Proof: Load proof Proof not loaded.
L7269 Theorem. (
pair_Sigma )
∀X : set , ∀Y : set → set , ∀x ∈ X , ∀y ∈ Y x , pair x y ∈ ∑ x ∈ X , Y x
Proof: Load proof Proof not loaded.
L7284 Theorem. (
pair_Sigma_E1 )
∀X : set , ∀Y : set → set , ∀x y : set , pair x y ∈ (∑ x ∈ X , Y x ) → y ∈ Y x
Proof: Load proof Proof not loaded.
L7295 Theorem. (
Sigma_E )
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑ x ∈ X , Y x ) → ∃x ∈ X , ∃y ∈ Y x , z = pair x y
Proof: Load proof Proof not loaded.
L7313 Definition. We define
setprod to be
λX Y : set ⇒ ∑ x ∈ X , Y of type
set → set → set .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
L7317 Let lam : set → (set → set ) → set ≝ Sigma
L7319 Definition. We define
ap to be
λf x ⇒ { proj1 z | z ∈ f , ∃y : set , z = pair x y } of type
set → set → set .
Notation . When
x is a set, a term
x y is notation for
ap x y .
Notation .
λ x ∈ A ⇒ B is notation for the set
Sigma A (λ x : set ⇒ B ).
Notation . We now use n-tuple notation (
a0 ,...,
an-1 ) for n ≥ 2 for λ i ∈
n .
if i = 0
then a0 else ... if i =
n-2 then an-2 else an-1 .
L7323 Theorem. (
lamI )
∀X : set , ∀F : set → set , ∀x ∈ X , ∀y ∈ F x , pair x y ∈ λ x ∈ X ⇒ F x
Proof: Load proof Proof not loaded.
L7327 Theorem. (
lamE )
∀X : set , ∀F : set → set , ∀z : set , z ∈ (λ x ∈ X ⇒ F x ) → ∃x ∈ X , ∃y ∈ F x , z = pair x y
Proof: Load proof Proof not loaded.
L7331 Theorem. (
apI )
∀f x y, pair x y ∈ f → y ∈ f x
Proof: Load proof Proof not loaded.
L7343 Theorem. (
apE )
∀f x y, y ∈ f x → pair x y ∈ f
Proof: Load proof Proof not loaded.
L7371 Theorem. (
beta )
∀X : set , ∀F : set → set , ∀x : set , x ∈ X → (λ x ∈ X ⇒ F x ) x = F x
Proof: Load proof Proof not loaded.
L7391
Proof: Load proof Proof not loaded.
L7411
Proof: Load proof Proof not loaded.
L7431
Proof: Load proof Proof not loaded.
L7438
Proof: Load proof Proof not loaded.
L7445 Theorem. (
ap0_Sigma )
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑ x ∈ X , Y x ) → (z 0 ) ∈ X
Proof: Load proof Proof not loaded.
L7451 Theorem. (
ap1_Sigma )
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑ x ∈ X , Y x ) → (z 1 ) ∈ (Y (z 0 ) )
Proof: Load proof Proof not loaded.
L7458 Definition. We define
pair_p to be
λu : set ⇒ pair (u 0 ) (u 1 ) = u of type
set → prop .
L7461
Proof: Load proof Proof not loaded.
L7469
Proof: Load proof Proof not loaded.
L7487
Proof: Load proof Proof not loaded.
L7562 Definition. We define
Pi to be
λX Y ⇒ { f ∈ 𝒫 (∑ x ∈ X , ⋃ (Y x ) ) | ∀x ∈ X , f x ∈ Y x } of type
set → (set → set ) → set .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
L7566 Theorem. (
PiI )
∀X : set , ∀Y : set → set , ∀f : set , (∀u ∈ f , pair_p u ∧ u 0 ∈ X ) → (∀x ∈ X , f x ∈ Y x ) → f ∈ ∏ x ∈ X , Y x
Proof: Load proof Proof not loaded.
L7600 Theorem. (
lam_Pi )
∀X : set , ∀Y : set → set , ∀F : set → set , (∀x ∈ X , F x ∈ Y x ) → (λ x ∈ X ⇒ F x ) ∈ (∏ x ∈ X , Y x )
Proof: Load proof Proof not loaded.
L7639 Theorem. (
ap_Pi )
∀X : set , ∀Y : set → set , ∀f : set , ∀x : set , f ∈ (∏ x ∈ X , Y x ) → x ∈ X → f x ∈ Y x
Proof: Load proof Proof not loaded.
L7645 Definition. We define
setexp to be
λX Y : set ⇒ ∏ y ∈ Y , X of type
set → set → set .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
L7649
Proof: Load proof Proof not loaded.
Beginning of Section Tuples
L7658 Variable x0 x1 : set
L7659
Proof: Load proof Proof not loaded.
L7664
Proof: Load proof Proof not loaded.
End of Section Tuples
L7671
Proof: Load proof Proof not loaded.
L7682 Theorem. (
lamI2 )
∀X, ∀F : set → set , ∀x ∈ X , ∀y ∈ F x , ( x ,y ) ∈ λ x ∈ X ⇒ F x
Proof: Load proof Proof not loaded.
L7688
Proof: Load proof Proof not loaded.
L7692
Proof: Load proof Proof not loaded.
End of Section pair_setsum
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
L7707 Definition. We define
DescrR_i_io_1 to be
λR ⇒ Eps_i (λx ⇒ (∃y : set → prop , R x y ) ∧ (∀y z : set → prop , R x y → R x z → y = z ) ) of type
(set → (set → prop ) → prop ) → set .
L7710
Proof: Load proof Proof not loaded.
L7720 Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀beta ∈ alpha , p beta ↔ q beta of type
set → (set → prop ) → (set → prop ) → prop .
L7726
Proof: Load proof Proof not loaded.
L7732
Proof: Load proof Proof not loaded.
L7740
Proof: Load proof Proof not loaded.
L7749
Proof: Load proof Proof not loaded.
L7759 Definition. We define
PNoLt_ to be
λalpha p q ⇒ ∃beta ∈ alpha , PNoEq_ beta p q ∧ ¬ p beta ∧ q beta of type
set → (set → prop ) → (set → prop ) → prop .
L7762
Proof: Load proof Proof not loaded.
L7773
Proof: Load proof Proof not loaded.
L7780
Proof: Load proof Proof not loaded.
L7791
Proof: Load proof Proof not loaded.
L7871
Proof: Load proof Proof not loaded.
L7880
Proof: Load proof Proof not loaded.
L7892
Proof: Load proof Proof not loaded.
L7904
Proof: Load proof Proof not loaded.
L7919
Proof: Load proof Proof not loaded.
L7930
Proof: Load proof Proof not loaded.
L7997
Proof: Load proof Proof not loaded.
L8051
Proof: Load proof Proof not loaded.
L8109
Proof: Load proof Proof not loaded.
L8424 Definition. We define
PNoLe to be
λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type
set → (set → prop ) → set → (set → prop ) → prop .
L8427
Proof: Load proof Proof not loaded.
L8435
Proof: Load proof Proof not loaded.
L8445
Proof: Load proof Proof not loaded.
L8451
Proof: Load proof Proof not loaded.
L8497
Proof: Load proof Proof not loaded.
L8514
Proof: Load proof Proof not loaded.
L8533
Proof: Load proof Proof not loaded.
L8552
Proof: Load proof Proof not loaded.
L8573 Definition. We define
PNo_downc to be
λL alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop , L beta q ∧ PNoLe alpha p beta q of type
(set → (set → prop ) → prop ) → set → (set → prop ) → prop .
L8576 Definition. We define
PNo_upc to be
λR alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop , R beta q ∧ PNoLe beta q alpha p of type
(set → (set → prop ) → prop ) → set → (set → prop ) → prop .
L8578
Proof: Load proof Proof not loaded.
L8598
Proof: Load proof Proof not loaded.
L8609 Theorem. (
PNo_upc_ref )
∀R : set → (set → prop ) → prop , ∀alpha, ordinal alpha → ∀p : set → prop , R alpha p → PNo_upc R alpha p
Proof: Load proof Proof not loaded.
L8620
Proof: Load proof Proof not loaded.
L8640 Definition. We define
PNoLt_pwise to be
λL R ⇒ ∀gamma, ordinal gamma → ∀p : set → prop , L gamma p → ∀delta, ordinal delta → ∀q : set → prop , R delta q → PNoLt gamma p delta q of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → prop .
L8643
Proof: Load proof Proof not loaded.
L8693
Proof: Load proof Proof not loaded.
L8710
Proof: Load proof Proof not loaded.
L8751
Proof: Load proof Proof not loaded.
L8768
Proof: Load proof Proof not loaded.
L8809
Proof: Load proof Proof not loaded.
L8819
Proof: Load proof Proof not loaded.
L8836
Proof: Load proof Proof not loaded.
L8853
Proof: Load proof Proof not loaded.
L8870
Proof: Load proof Proof not loaded.
L9947 Definition. We define
PNo_lenbdd to be
λalpha L ⇒ ∀beta, ∀p : set → prop , L beta p → beta ∈ alpha of type
set → (set → (set → prop ) → prop ) → prop .
L9950
Proof: Load proof Proof not loaded.
L10087
Proof: Load proof Proof not loaded.
L10229
Proof: Load proof Proof not loaded.
L10245
Proof: Load proof Proof not loaded.
L10288
Proof: Load proof Proof not loaded.
L10303
Proof: Load proof Proof not loaded.
L10318
Proof: Load proof Proof not loaded.
L10328
Proof: Load proof Proof not loaded.
L10409
Proof: Load proof Proof not loaded.
L10488
Proof: Load proof Proof not loaded.
L10507
Proof: Load proof Proof not loaded.
L10753
Proof: Load proof Proof not loaded.
L10785 Definition. We define
PNo_least_rep2 to be
λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta → ¬ p x of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → set → (set → prop ) → prop .
L10787
Proof: Load proof Proof not loaded.
L10883
Proof: Load proof Proof not loaded.
L10976
Proof: Load proof Proof not loaded.
L10988
Proof: Load proof Proof not loaded.
L10999
Proof: Load proof Proof not loaded.
Beginning of Section TaggedSets
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
L11035
Proof: Load proof Proof not loaded.
L11043
Proof: Load proof Proof not loaded.
L11047
Proof: Load proof Proof not loaded.
L11059
Proof: Load proof Proof not loaded.
L11066
Proof: Load proof Proof not loaded.
L11087
Proof: Load proof Proof not loaded.
L11095
Proof: Load proof Proof not loaded.
L11108
Proof: Load proof Proof not loaded.
L11122 Definition. We define
SNoElts_ to be
λalpha ⇒ alpha ∪ { beta ' | beta ∈ alpha } of type
set → set .
L11124
Proof: Load proof Proof not loaded.
L11154
Proof: Load proof Proof not loaded.
L11181
Proof: Load proof Proof not loaded.
L11261
Proof: Load proof Proof not loaded.
L11328 Definition. We define
SNo to be
λx ⇒ ∃alpha, ordinal alpha ∧ SNo_ alpha x of type
set → prop .
L11329
Proof: Load proof Proof not loaded.
L11341
Proof: Load proof Proof not loaded.
L11374
Proof: Load proof Proof not loaded.
L11381
Proof: Load proof Proof not loaded.
L11387
Proof: Load proof Proof not loaded.
L11391
Proof: Load proof Proof not loaded.
L11395
Proof: Load proof Proof not loaded.
L11405
Proof: Load proof Proof not loaded.
L11422
Proof: Load proof Proof not loaded.
L11467 Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) of type
set → set → set → prop .
L11470
Proof: Load proof Proof not loaded.
L11474
Proof: Load proof Proof not loaded.
End of Section TaggedSets
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 .
L11501
Proof: Load proof Proof not loaded.
L11508
Proof: Load proof Proof not loaded.
L11522
Proof: Load proof Proof not loaded.
L11527
Proof: Load proof Proof not loaded.
L11532
Proof: Load proof Proof not loaded.
L11635
Proof: Load proof Proof not loaded.
L11650
Proof: Load proof Proof not loaded.
L11664
Proof: Load proof Proof not loaded.
L11669
Proof: Load proof Proof not loaded.
L11680
Proof: Load proof Proof not loaded.
L11693
Proof: Load proof Proof not loaded.
L11699
Proof: Load proof Proof not loaded.
L11703
Proof: Load proof Proof not loaded.
L11711
Proof: Load proof Proof not loaded.
L11716
Proof: Load proof Proof not loaded.
L11721
Proof: Load proof Proof not loaded.
L11726
Proof: Load proof Proof not loaded.
L11735
Proof: Load proof Proof not loaded.
L11758
Proof: Load proof Proof not loaded.
L11784 Definition. We define
SNoCutP to be
λL R ⇒ (∀x ∈ L , SNo x ) ∧ (∀y ∈ R , SNo y ) ∧ (∀x ∈ L , ∀y ∈ R , x < y ) of type
set → set → prop .
L11789
Proof: Load proof Proof not loaded.
L12178
Proof: Load proof Proof not loaded.
L12193
Proof: Load proof Proof not loaded.
L12204
Proof: Load proof Proof not loaded.
L12210
Proof: Load proof Proof not loaded.
Beginning of Section TaggedSets2
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
L12222
Proof: Load proof Proof not loaded.
L12247
Proof: Load proof Proof not loaded.
L12253
Proof: Load proof Proof not loaded.
L12263
Proof: Load proof Proof not loaded.
L12276
Proof: Load proof Proof not loaded.
L12300
Proof: Load proof Proof not loaded.
L12316
Proof: Load proof Proof not loaded.
L12327
Proof: Load proof Proof not loaded.
L12375
Proof: Load proof Proof not loaded.
L12393
Proof: Load proof Proof not loaded.
L12411
Proof: Load proof Proof not loaded.
L12415
Proof: Load proof Proof not loaded.
L12419
Proof: Load proof Proof not loaded.
L12429
Proof: Load proof Proof not loaded.
L12439
Proof: Load proof Proof not loaded.
L12449
Proof: Load proof Proof not loaded.
L12459
Proof: Load proof Proof not loaded.
L12533
Proof: Load proof Proof not loaded.
L12542
Proof: Load proof Proof not loaded.
L12550
Proof: Load proof Proof not loaded.
L12557
Proof: Load proof Proof not loaded.
L12569
Proof: Load proof Proof not loaded.
L12672
Proof: Load proof Proof not loaded.
L12695
Proof: Load proof Proof not loaded.
L12717
Proof: Load proof Proof not loaded.
L12743
Proof: Load proof Proof not loaded.
L12783
Proof: Load proof Proof not loaded.
L12823
Proof: Load proof Proof not loaded.
L12846
Proof: Load proof Proof not loaded.
L12855
Proof: Load proof Proof not loaded.
L12864
Proof: Load proof Proof not loaded.
L12911
Proof: Load proof Proof not loaded.
L12943
Proof: Load proof Proof not loaded.
L12965
Proof: Load proof Proof not loaded.
L12973
Proof: Load proof Proof not loaded.
L12980
Proof: Load proof Proof not loaded.
L12988
Proof: Load proof Proof not loaded.
L13004
Proof: Load proof Proof not loaded.
L13083
Proof: Load proof Proof not loaded.
L13105
Proof: Load proof Proof not loaded.
L13118
Proof: Load proof Proof not loaded.
L13124
Proof: Load proof Proof not loaded.
L13128
Proof: Load proof Proof not loaded.
L13132
Proof: Load proof Proof not loaded.
L13136
Proof: Load proof Proof not loaded.
L13140
Proof: Load proof Proof not loaded.
L13165
Proof: Load proof Proof not loaded.
L13180
Proof: Load proof Proof not loaded.
L13195
Proof: Load proof Proof not loaded.
L13231
Proof: Load proof Proof not loaded.
L13235
Proof: Load proof Proof not loaded.
L13282
Proof: Load proof Proof not loaded.
L13291
Proof: Load proof Proof not loaded.
L13341
Proof: Load proof Proof not loaded.
L13349
Proof: Load proof Proof not loaded.
L13357
Proof: Load proof Proof not loaded.
L13364
Proof: Load proof Proof not loaded.
L13371
Proof: Load proof Proof not loaded.
L13378
Proof: Load proof Proof not loaded.
L13385
Proof: Load proof Proof not loaded.
L13408
Proof: Load proof Proof not loaded.
L13420
Proof: Load proof Proof not loaded.
L13444
Proof: Load proof Proof not loaded.
L13468
Proof: Load proof Proof not loaded.
L13481
Proof: Load proof Proof not loaded.
L13496
Proof: Load proof Proof not loaded.
L13511
Proof: Load proof Proof not loaded.
L13609
Proof: Load proof Proof not loaded.
L13616
Proof: Load proof Proof not loaded.
L13620
Proof: Load proof Proof not loaded.
L13627
Proof: Load proof Proof not loaded.
L13634
Proof: Load proof Proof not loaded.
L13672
Proof: Load proof Proof not loaded.
L13689
Proof: Load proof Proof not loaded.
L13736
Proof: Load proof Proof not loaded.
L13782
Proof: Load proof Proof not loaded.
L13840
Proof: Load proof Proof not loaded.
L13867
Proof: Load proof Proof not loaded.
End of Section TaggedSets2
L14047
Proof: Load proof Proof not loaded.
L14158
Proof: Load proof Proof not loaded.
Beginning of Section SurrealRecI
L14211 Variable F : set → (set → set ) → set
L14225 Hypothesis Fr : ∀z, SNo z → ∀g h : set → set , (∀w ∈ SNoS_ (SNoLev z ) , g w = h w ) → F z g = F z h
L14228
Proof: Load proof Proof not loaded.
End of Section SurrealRecI
Beginning of Section SurrealRecII
L14305 Variable F : set → (set → (set → set ) ) → (set → set )
L14307 Let G : set → (set → set → (set → set ) ) → set → (set → set ) ≝ λalpha g ⇒ If_iii (ordinal alpha ) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ g (SNoLev w ) w ) ) default ) (λz : set ⇒ default )
L14318 Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set ) , (∀w ∈ SNoS_ (SNoLev z ) , g w = h w ) → F z g = F z h
L14321
Proof: Load proof Proof not loaded.
End of Section SurrealRecII
Beginning of Section SurrealRec2
L14398 Variable F : set → set → (set → set → set ) → set
L14399 Let G : set → (set → set → set ) → set → (set → set ) → set ≝ λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y )
L14411
Proof: Load proof Proof not loaded.
L14448
Proof: Load proof Proof not loaded.
L14462
Proof: Load proof Proof not loaded.
End of Section SurrealRec2
L14559
Proof: Load proof Proof not loaded.
L14575
Proof: Load proof Proof not loaded.
L14603
Proof: Load proof Proof not loaded.
L14640
Proof: Load proof Proof not loaded.
L14663
Proof: Load proof Proof not loaded.
L14709 Theorem. (
SNoLev_ind3 )
∀P : set → set → set → prop , (∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x ) , P u y z ) → (∀v ∈ SNoS_ (SNoLev y ) , P x v z ) → (∀w ∈ SNoS_ (SNoLev z ) , P x y w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , P u v z ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀w ∈ SNoS_ (SNoLev z ) , P u y w ) → (∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , P x v w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , P u v w ) → P x y z ) → ∀x y z, SNo x → SNo y → SNo z → P x y z
Proof: Load proof Proof not loaded.
L14788
Proof: Load proof Proof not loaded.
L14792
Proof: Load proof Proof not loaded.
L14798
Proof: Load proof Proof not loaded.
L14804
Proof: Load proof Proof not loaded.
L14810
Proof: Load proof Proof not loaded.
L14850
Proof: Load proof Proof not loaded.
L14859
Proof: Load proof Proof not loaded.
L14868
Proof: Load proof Proof not loaded.
L14884
Proof: Load proof Proof not loaded.
L14909
Proof: Load proof Proof not loaded.
Beginning of Section SurrealMinus
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 .
L14944
Proof: Load proof Proof not loaded.
L14975
Proof: Load proof Proof not loaded.
L15166
Proof: Load proof Proof not loaded.
L15173
Proof: Load proof Proof not loaded.
L15242
Proof: Load proof Proof not loaded.
L15260
Proof: Load proof Proof not loaded.
L15268
Proof: Load proof Proof not loaded.
L15319
Proof: Load proof Proof not loaded.
L15490
Proof: Load proof Proof not loaded.
L15501
Proof: Load proof Proof not loaded.
L15569
Proof: Load proof Proof not loaded.
L15580
Proof: Load proof Proof not loaded.
L15597
Proof: Load proof Proof not loaded.
L15610
Proof: Load proof Proof not loaded.
L15720
Proof: Load proof Proof not loaded.
L15725
Proof: Load proof Proof not loaded.
L15738
Proof: Load proof Proof not loaded.
L15751
Proof: Load proof Proof not loaded.
L15767
Proof: Load proof Proof not loaded.
L15783
Proof: Load proof Proof not loaded.
End of Section SurrealMinus
Beginning of Section SurrealAdd
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 .
L15834
Proof: Load proof Proof not loaded.
L15890
Proof: Load proof Proof not loaded.
L16351
Proof: Load proof Proof not loaded.
L16361
Proof: Load proof Proof not loaded.
L16370
Proof: Load proof Proof not loaded.
L16378
Proof: Load proof Proof not loaded.
L16383
Proof: Load proof Proof not loaded.
L16448
Proof: Load proof Proof not loaded.
L16460
Proof: Load proof Proof not loaded.
L16526
Proof: Load proof Proof not loaded.
L16538
Proof: Load proof Proof not loaded.
L16551
Proof: Load proof Proof not loaded.
L16564
Proof: Load proof Proof not loaded.
L16579
Proof: Load proof Proof not loaded.
L16592
Proof: Load proof Proof not loaded.
L16600
Proof: Load proof Proof not loaded.
L16701
Proof: Load proof Proof not loaded.
L16764
Proof: Load proof Proof not loaded.
L16770
Proof: Load proof Proof not loaded.
L16945
Proof: Load proof Proof not loaded.
L16955
Proof: Load proof Proof not loaded.
L16995
Proof: Load proof Proof not loaded.
L17027
Proof: Load proof Proof not loaded.
L17092
Proof: Load proof Proof not loaded.
L17244
Proof: Load proof Proof not loaded.
L17265
Proof: Load proof Proof not loaded.
L17289
Proof: Load proof Proof not loaded.
L17306
Proof: Load proof Proof not loaded.
L17335
Proof: Load proof Proof not loaded.
L17344
Proof: Load proof Proof not loaded.
L17349
Proof: Load proof Proof not loaded.
L17506
Proof: Load proof Proof not loaded.
L17663
Proof: Load proof Proof not loaded.
L18079
Proof: Load proof Proof not loaded.
L18088
Proof: Load proof Proof not loaded.
L18094
Proof: Load proof Proof not loaded.
L18103
Proof: Load proof Proof not loaded.
L18109
Proof: Load proof Proof not loaded.
L18122
Proof: Load proof Proof not loaded.
L18136
Proof: Load proof Proof not loaded.
L18144
Proof: Load proof Proof not loaded.
L18174
Proof: Load proof Proof not loaded.
L18182
Proof: Load proof Proof not loaded.
L18546
Proof: Load proof Proof not loaded.
L18576
Proof: Load proof Proof not loaded.
L18592
Proof: Load proof Proof not loaded.
L18599
Proof: Load proof Proof not loaded.
L18615
Proof: Load proof Proof not loaded.
L18625
Proof: Load proof Proof not loaded.
L18635
Proof: Load proof Proof not loaded.
L18645
Proof: Load proof Proof not loaded.
L18657
Proof: Load proof Proof not loaded.
L18671
Proof: Load proof Proof not loaded.
L18679
Proof: Load proof Proof not loaded.
L18687
Proof: Load proof Proof not loaded.
L18695
Proof: Load proof Proof not loaded.
L18704
Proof: Load proof Proof not loaded.
L18715
Proof: Load proof Proof not loaded.
L18723
Proof: Load proof Proof not loaded.
L18733
Proof: Load proof Proof not loaded.
L18744
Proof: Load proof Proof not loaded.
L18754
Proof: Load proof Proof not loaded.
L18764
Proof: Load proof Proof not loaded.
L18773
Proof: Load proof Proof not loaded.
L18782
Proof: Load proof Proof not loaded.
L18812
Proof: Load proof Proof not loaded.
L18825
Proof: Load proof Proof not loaded.
L18838
Proof: Load proof Proof not loaded.
L18869
Proof: Load proof Proof not loaded.
L18892
Proof: Load proof Proof not loaded.
L18909
Proof: Load proof Proof not loaded.
L18943
Proof: Load proof Proof not loaded.
L19003
Proof: Load proof Proof not loaded.
L19011
Proof: Load proof Proof not loaded.
L19024
Proof: Load proof Proof not loaded.
L19034
Proof: Load proof Proof not loaded.
L19042
Proof: Load proof Proof not loaded.
L19050
Proof: Load proof Proof not loaded.
L19057
Proof: Load proof Proof not loaded.
L19083
Proof: Load proof Proof not loaded.
L19092
Proof: Load proof Proof not loaded.
L19101
Proof: Load proof Proof not loaded.
L19109
Proof: Load proof Proof not loaded.
L19132
Proof: Load proof Proof not loaded.
L19142
Proof: Load proof Proof not loaded.
L19151
Proof: Load proof Proof not loaded.
End of Section SurrealAdd
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 .
L19185
Proof: Load proof Proof not loaded.
L19190
Proof: Load proof Proof not loaded.
L19195
Proof: Load proof Proof not loaded.
L19201
Proof: Load proof Proof not loaded.
L19211
Proof: Load proof Proof not loaded.
L19219
Proof: Load proof Proof not loaded.
L19251
Proof: Load proof Proof not loaded.
End of Section SurrealAbs
Beginning of Section SurrealMul
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 .
L19289
Proof: Load proof Proof not loaded.
L19449 Theorem. (
mul_SNo_eq_2 )
∀x y, SNo x → SNo y → ∀p : prop , (∀L R, (∀u, u ∈ L → (∀q : prop , (∀w0 ∈ SNoL x , ∀w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 → q ) → (∀z0 ∈ SNoR x , ∀z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 → q ) → q ) ) → (∀w0 ∈ SNoL x , ∀w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L ) → (∀z0 ∈ SNoR x , ∀z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L ) → (∀u, u ∈ R → (∀q : prop , (∀w0 ∈ SNoL x , ∀z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 → q ) → (∀z0 ∈ SNoR x , ∀w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 → q ) → q ) ) → (∀w0 ∈ SNoL x , ∀z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R ) → (∀z0 ∈ SNoR x , ∀w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R ) → x * y = SNoCut L R → p ) → p
Proof: Load proof Proof not loaded.
L19565 Theorem. (
mul_SNo_prop_1 )
∀x, SNo x → ∀y, SNo y → ∀p : prop , (SNo (x * y ) → (∀u ∈ SNoL x , ∀v ∈ SNoL y , u * y + x * v < x * y + u * v ) → (∀u ∈ SNoR x , ∀v ∈ SNoR y , u * y + x * v < x * y + u * v ) → (∀u ∈ SNoL x , ∀v ∈ SNoR y , x * y + u * v < u * y + x * v ) → (∀u ∈ SNoR x , ∀v ∈ SNoL y , x * y + u * v < u * y + x * v ) → p ) → p
Proof: Load proof Proof not loaded.
L20606
Proof: Load proof Proof not loaded.
L20611
Proof: Load proof Proof not loaded.
L20625
Proof: Load proof Proof not loaded.
L20634 Theorem. (
mul_SNo_eq_3 )
∀x y, SNo x → SNo y → ∀p : prop , (∀L R, SNoCutP L R → (∀u, u ∈ L → (∀q : prop , (∀w0 ∈ SNoL x , ∀w1 ∈ SNoL y , u = w0 * y + x * w1 + - w0 * w1 → q ) → (∀z0 ∈ SNoR x , ∀z1 ∈ SNoR y , u = z0 * y + x * z1 + - z0 * z1 → q ) → q ) ) → (∀w0 ∈ SNoL x , ∀w1 ∈ SNoL y , w0 * y + x * w1 + - w0 * w1 ∈ L ) → (∀z0 ∈ SNoR x , ∀z1 ∈ SNoR y , z0 * y + x * z1 + - z0 * z1 ∈ L ) → (∀u, u ∈ R → (∀q : prop , (∀w0 ∈ SNoL x , ∀z1 ∈ SNoR y , u = w0 * y + x * z1 + - w0 * z1 → q ) → (∀z0 ∈ SNoR x , ∀w1 ∈ SNoL y , u = z0 * y + x * w1 + - z0 * w1 → q ) → q ) ) → (∀w0 ∈ SNoL x , ∀z1 ∈ SNoR y , w0 * y + x * z1 + - w0 * z1 ∈ R ) → (∀z0 ∈ SNoR x , ∀w1 ∈ SNoL y , z0 * y + x * w1 + - z0 * w1 ∈ R ) → x * y = SNoCut L R → p ) → p
Proof: Load proof Proof not loaded.
L20875
Proof: Load proof Proof not loaded.
L21231
Proof: Load proof Proof not loaded.
L21250
Proof: Load proof Proof not loaded.
L21432
Proof: Load proof Proof not loaded.
L21454
Proof: Load proof Proof not loaded.
L21636
Proof: Load proof Proof not loaded.
L21658 Theorem. (
mul_SNo_Subq_lem )
∀x y X Y Z W, ∀U U', (∀u, u ∈ U → (∀q : prop , (∀w0 ∈ X , ∀w1 ∈ Y , u = w0 * y + x * w1 + - w0 * w1 → q ) → (∀z0 ∈ Z , ∀z1 ∈ W , u = z0 * y + x * z1 + - z0 * z1 → q ) → q ) ) → (∀w0 ∈ X , ∀w1 ∈ Y , w0 * y + x * w1 + - w0 * w1 ∈ U' ) → (∀w0 ∈ Z , ∀w1 ∈ W , w0 * y + x * w1 + - w0 * w1 ∈ U' ) → U ⊆ U'
Proof: Load proof Proof not loaded.
L21681
Proof: Load proof Proof not loaded.
L21723
Proof: Load proof Proof not loaded.
L21851
Proof: Load proof Proof not loaded.
L22010
Proof: Load proof Proof not loaded.
L22402
Proof: Load proof Proof not loaded.
L22409
Proof: Load proof Proof not loaded.
L23722
Proof: Load proof Proof not loaded.
Beginning of Section mul_SNo_assoc_lems
L23737 Variable M : set → set → set
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
M .
L23739 Hypothesis SNo_M : ∀x y, SNo x → SNo y → SNo (x * y )
L23740 Hypothesis DL : ∀x y z, SNo x → SNo y → SNo z → x * (y + z ) = x * y + x * z
L23741 Hypothesis DR : ∀x y z, SNo x → SNo y → SNo z → (x + y ) * z = x * z + y * z
L23752 Hypothesis M_Lt : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v
L23754 Hypothesis M_Le : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v
L23756 Theorem. (
mul_SNo_assoc_lem1 )
∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x ) , u * (y * z ) = (u * y ) * z ) → (∀v ∈ SNoS_ (SNoLev y ) , x * (v * z ) = (x * v ) * z ) → (∀w ∈ SNoS_ (SNoLev z ) , x * (y * w ) = (x * y ) * w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , u * (v * z ) = (u * v ) * z ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀w ∈ SNoS_ (SNoLev z ) , u * (y * w ) = (u * y ) * w ) → (∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , x * (v * w ) = (x * v ) * w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , u * (v * w ) = (u * v ) * w ) → ∀L, (∀u ∈ L , ∀q : prop , (∀v ∈ SNoL x , ∀w ∈ SNoL (y * z ) , u = v * (y * z ) + x * w + - v * w → q ) → (∀v ∈ SNoR x , ∀w ∈ SNoR (y * z ) , u = v * (y * z ) + x * w + - v * w → q ) → q ) → ∀u ∈ L , u < (x * y ) * z
Proof: Load proof Proof not loaded.
L24216 Theorem. (
mul_SNo_assoc_lem2 )
∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x ) , u * (y * z ) = (u * y ) * z ) → (∀v ∈ SNoS_ (SNoLev y ) , x * (v * z ) = (x * v ) * z ) → (∀w ∈ SNoS_ (SNoLev z ) , x * (y * w ) = (x * y ) * w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , u * (v * z ) = (u * v ) * z ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀w ∈ SNoS_ (SNoLev z ) , u * (y * w ) = (u * y ) * w ) → (∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , x * (v * w ) = (x * v ) * w ) → (∀u ∈ SNoS_ (SNoLev x ) , ∀v ∈ SNoS_ (SNoLev y ) , ∀w ∈ SNoS_ (SNoLev z ) , u * (v * w ) = (u * v ) * w ) → ∀R, (∀u ∈ R , ∀q : prop , (∀v ∈ SNoL x , ∀w ∈ SNoR (y * z ) , u = v * (y * z ) + x * w + - v * w → q ) → (∀v ∈ SNoR x , ∀w ∈ SNoL (y * z ) , u = v * (y * z ) + x * w + - v * w → q ) → q ) → ∀u ∈ R , (x * y ) * z < u
Proof: Load proof Proof not loaded.
End of Section mul_SNo_assoc_lems
L24701
Proof: Load proof Proof not loaded.
L24916
Proof: Load proof Proof not loaded.
L24958
Proof: Load proof Proof not loaded.
L24964
Proof: Load proof Proof not loaded.
L24970
Proof: Load proof Proof not loaded.
L24976
Proof: Load proof Proof not loaded.
L24990
Proof: Load proof Proof not loaded.
L25008
Proof: Load proof Proof not loaded.
L25026
Proof: Load proof Proof not loaded.
L25044
Proof: Load proof Proof not loaded.
L25051
Proof: Load proof Proof not loaded.
L25058
Proof: Load proof Proof not loaded.
L25065
Proof: Load proof Proof not loaded.
L25072
Proof: Load proof Proof not loaded.
L25087
Proof: Load proof Proof not loaded.
L25102
Proof: Load proof Proof not loaded.
L25118
Proof: Load proof Proof not loaded.
L25132
Proof: Load proof Proof not loaded.
L25146
Proof: Load proof Proof not loaded.
L25162
Proof: Load proof Proof not loaded.
L25178
Proof: Load proof Proof not loaded.
L25195
Proof: Load proof Proof not loaded.
L25212
Proof: Load proof Proof not loaded.
L25240
Proof: Load proof Proof not loaded.
L25258
Proof: Load proof Proof not loaded.
L25277
Proof: Load proof Proof not loaded.
L25302
Proof: Load proof Proof not loaded.
L25328
Proof: Load proof Proof not loaded.
L25337
Proof: Load proof Proof not loaded.
L25347
Proof: Load proof Proof not loaded.
L25357
Proof: Load proof Proof not loaded.
L25369
Proof: Load proof Proof not loaded.
L25384
Proof: Load proof Proof not loaded.
L25420 Theorem. (
mul_SNoCutP_lem )
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → SNoCutP ({ w 0 * y + x * w 1 + - w 0 * w 1 | w ∈ Lx ⨯ Ly } ∪ { z 0 * y + x * z 1 + - z 0 * z 1 | z ∈ Rx ⨯ Ry } ) ({ w 0 * y + x * w 1 + - w 0 * w 1 | w ∈ Lx ⨯ Ry } ∪ { z 0 * y + x * z 1 + - z 0 * z 1 | z ∈ Rx ⨯ Ly } ) ∧ x * y = SNoCut ({ w 0 * y + x * w 1 + - w 0 * w 1 | w ∈ Lx ⨯ Ly } ∪ { z 0 * y + x * z 1 + - z 0 * z 1 | z ∈ Rx ⨯ Ry } ) ({ w 0 * y + x * w 1 + - w 0 * w 1 | w ∈ Lx ⨯ Ry } ∪ { z 0 * y + x * z 1 + - z 0 * z 1 | z ∈ Rx ⨯ Ly } ) ∧ ∀q : prop , (∀LxLy' RxRy' LxRy' RxLy', (∀u ∈ LxLy' , ∀p : prop , (∀w ∈ Lx , ∀w' ∈ Ly , SNo w → SNo w' → w < x → w' < y → u = w * y + x * w' + - w * w' → p ) → p ) → (∀w ∈ Lx , ∀w' ∈ Ly , w * y + x * w' + - w * w' ∈ LxLy' ) → (∀u ∈ RxRy' , ∀p : prop , (∀z ∈ Rx , ∀z' ∈ Ry , SNo z → SNo z' → x < z → y < z' → u = z * y + x * z' + - z * z' → p ) → p ) → (∀z ∈ Rx , ∀z' ∈ Ry , z * y + x * z' + - z * z' ∈ RxRy' ) → (∀u ∈ LxRy' , ∀p : prop , (∀w ∈ Lx , ∀z ∈ Ry , SNo w → SNo z → w < x → y < z → u = w * y + x * z + - w * z → p ) → p ) → (∀w ∈ Lx , ∀z ∈ Ry , w * y + x * z + - w * z ∈ LxRy' ) → (∀u ∈ RxLy' , ∀p : prop , (∀z ∈ Rx , ∀w ∈ Ly , SNo z → SNo w → x < z → w < y → u = z * y + x * w + - z * w → p ) → p ) → (∀z ∈ Rx , ∀w ∈ Ly , z * y + x * w + - z * w ∈ RxLy' ) → SNoCutP (LxLy' ∪ RxRy' ) (LxRy' ∪ RxLy' ) → x * y = SNoCut (LxLy' ∪ RxRy' ) (LxRy' ∪ RxLy' ) → q ) → q
Proof: Load proof Proof not loaded.
L26713 Theorem. (
mul_SNoCut_abs )
∀Lx Rx Ly Ry x y, SNoCutP Lx Rx → SNoCutP Ly Ry → x = SNoCut Lx Rx → y = SNoCut Ly Ry → ∀q : prop , (∀LxLy' RxRy' LxRy' RxLy', (∀u ∈ LxLy' , ∀p : prop , (∀w ∈ Lx , ∀w' ∈ Ly , SNo w → SNo w' → w < x → w' < y → u = w * y + x * w' + - w * w' → p ) → p ) → (∀w ∈ Lx , ∀w' ∈ Ly , w * y + x * w' + - w * w' ∈ LxLy' ) → (∀u ∈ RxRy' , ∀p : prop , (∀z ∈ Rx , ∀z' ∈ Ry , SNo z → SNo z' → x < z → y < z' → u = z * y + x * z' + - z * z' → p ) → p ) → (∀z ∈ Rx , ∀z' ∈ Ry , z * y + x * z' + - z * z' ∈ RxRy' ) → (∀u ∈ LxRy' , ∀p : prop , (∀w ∈ Lx , ∀z ∈ Ry , SNo w → SNo z → w < x → y < z → u = w * y + x * z + - w * z → p ) → p ) → (∀w ∈ Lx , ∀z ∈ Ry , w * y + x * z + - w * z ∈ LxRy' ) → (∀u ∈ RxLy' , ∀p : prop , (∀z ∈ Rx , ∀w ∈ Ly , SNo z → SNo w → x < z → w < y → u = z * y + x * w + - z * w → p ) → p ) → (∀z ∈ Rx , ∀w ∈ Ly , z * y + x * w + - z * w ∈ RxLy' ) → SNoCutP (LxLy' ∪ RxRy' ) (LxRy' ∪ RxLy' ) → x * y = SNoCut (LxLy' ∪ RxRy' ) (LxRy' ∪ RxLy' ) → q ) → q
Proof: Load proof Proof not loaded.
L26738
Proof: Load proof Proof not loaded.
L26978
Proof: Load proof Proof not loaded.
L27004
Proof: Load proof Proof not loaded.
L27244
Proof: Load proof Proof not loaded.
L27270
Proof: Load proof Proof not loaded.
L27302
Proof: Load proof Proof not loaded.
End of Section SurrealMul
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 .
L27322 Definition. We define
int to be
ω ∪ { - n | n ∈ ω } of type
set .
L27324
Proof: Load proof Proof not loaded.
L27338
Proof: Load proof Proof not loaded.
L27367
Proof: Load proof Proof not loaded.
L27375
Proof: Load proof Proof not loaded.
L27382
Proof: Load proof Proof not loaded.
L27390
Proof: Load proof Proof not loaded.
L27446
Proof: Load proof Proof not loaded.
L27475
Proof: Load proof Proof not loaded.
L27484
Proof: Load proof Proof not loaded.
L27553
Proof: Load proof Proof not loaded.
End of Section Int
Beginning of Section BezoutAndGCD
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
L27591
Proof: Load proof Proof not loaded.
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 .
L27672
Proof: Load proof Proof not loaded.
L27683
Proof: Load proof Proof not loaded.
L27692
Proof: Load proof Proof not loaded.
L27699
Proof: Load proof Proof not loaded.
L27844
Proof: Load proof Proof not loaded.
L27859
Proof: Load proof Proof not loaded.
L27876
Proof: Load proof Proof not loaded.
L27913
Proof: Load proof Proof not loaded.
L27951
Proof: Load proof Proof not loaded.
L27973
Proof: Load proof Proof not loaded.
L28027
Proof: Load proof Proof not loaded.
L28051
Proof: Load proof Proof not loaded.
L28081
Proof: Load proof Proof not loaded.
L28094
Proof: Load proof Proof not loaded.
L28106
Proof: Load proof Proof not loaded.
L28191
Proof: Load proof Proof not loaded.
L28220
Proof: Load proof Proof not loaded.
L28231
Proof: Load proof Proof not loaded.
L28247
Proof: Load proof Proof not loaded.
L28253
Proof: Load proof Proof not loaded.
L28259
Proof: Load proof Proof not loaded.
L28265
Proof: Load proof Proof not loaded.
L28274
Proof: Load proof Proof not loaded.
L28474
Proof: Load proof Proof not loaded.
L28495
Proof: Load proof Proof not loaded.
L28653
Proof: Load proof Proof not loaded.
L28733
Proof: Load proof Proof not loaded.
L28764
Proof: Load proof Proof not loaded.
L28863
Proof: Load proof Proof not loaded.
L28890
Proof: Load proof Proof not loaded.
L28905
Proof: Load proof Proof not loaded.
L28928
Proof: Load proof Proof not loaded.
L28964 Theorem. (
euclidean_algorithm )
(∀m ∈ ω ∖ { 0 } , gcd_reln m m m ) ∧ (∀m ∈ ω ∖ { 0 } , gcd_reln 0 m m ) ∧ (∀m ∈ ω ∖ { 0 } , gcd_reln m 0 m ) ∧ (∀m n ∈ ω , m < n → ∀d, gcd_reln m (n + - m ) d → gcd_reln m n d ) ∧ (∀m n ∈ ω , n < m → ∀d, gcd_reln n m d → gcd_reln m n d ) ∧ (∀m ∈ ω , ∀n ∈ int , n < 0 → ∀d, gcd_reln m (- n ) d → gcd_reln m n d ) ∧ (∀m n ∈ int , m < 0 → ∀d, gcd_reln (- m ) n d → gcd_reln m n d )
Proof: Load proof Proof not loaded.
L29011
Proof: Load proof Proof not loaded.
End of Section BezoutAndGCD
Beginning of Section PrimeFactorization
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 .
L29133
Proof: Load proof Proof not loaded.
L29157 Definition. We define
Pi_SNo to be
λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i ) n of type
(set → set ) → set → set .
L29160
Proof: Load proof Proof not loaded.
L29165
Proof: Load proof Proof not loaded.
L29171
Proof: Load proof Proof not loaded.
L29196
Proof: Load proof Proof not loaded.
L29221
Proof: Load proof Proof not loaded.
L29246
Proof: Load proof Proof not loaded.
L29287
Proof: Load proof Proof not loaded.
L29301
Proof: Load proof Proof not loaded.
L29308
Proof: Load proof Proof not loaded.
L29340 Definition. We define
nonincrfinseq to be
λA n f ⇒ ∀i ∈ n , A (f i ) ∧ ∀j ∈ i , f i ≤ f j of type
(set → prop ) → set → (set → set ) → prop .
L29342
Proof: Load proof Proof not loaded.
L29365
Proof: Load proof Proof not loaded.
End of Section PrimeFactorization
Beginning of Section SurrealExp
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 .
L29867
Proof: Load proof Proof not loaded.
L29872
Proof: Load proof Proof not loaded.
L29877
Proof: Load proof Proof not loaded.
L29886
Proof: Load proof Proof not loaded.
L29896
Proof: Load proof Proof not loaded.
L29911
Proof: Load proof Proof not loaded.
L30071
Proof: Load proof Proof not loaded.
L30077
Proof: Load proof Proof not loaded.
L30086
Proof: Load proof Proof not loaded.
L30107
Proof: Load proof Proof not loaded.
L30127
Proof: Load proof Proof not loaded.
L30161
Proof: Load proof Proof not loaded.
L30186
Proof: Load proof Proof not loaded.
L30204
Proof: Load proof Proof not loaded.
L30213
Proof: Load proof Proof not loaded.
L30245
Proof: Load proof Proof not loaded.
L30250
Proof: Load proof Proof not loaded.
L30264
Proof: Load proof Proof not loaded.
L30314
Proof: Load proof Proof not loaded.
L30711
Proof: Load proof Proof not loaded.
L30763
Proof: Load proof Proof not loaded.
L30783
Proof: Load proof Proof not loaded.
End of Section SurrealExp
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 .
L30816 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 .
L30817 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 .
L30818
Proof: Load proof Proof not loaded.
L30839
Proof: Load proof Proof not loaded.
L30858
Proof: Load proof Proof not loaded.
L30879
Proof: Load proof Proof not loaded.
L31071
Proof: Load proof Proof not loaded.
L31141
Proof: Load proof Proof not loaded.
L31287
Proof: Load proof Proof not loaded.
L31355
Proof: Load proof Proof not loaded.
L31370
Proof: Load proof Proof not loaded.
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 .
L31396
Proof: Load proof Proof not loaded.
L31422
Proof: Load proof Proof not loaded.
L31447
Proof: Load proof Proof not loaded.
L31458
Proof: Load proof Proof not loaded.
L31463
Proof: Load proof Proof not loaded.
L31475
Proof: Load proof Proof not loaded.
L31501
Proof: Load proof Proof not loaded.
L31543
Proof: Load proof Proof not loaded.
L31621
Proof: Load proof Proof not loaded.
L31826
Proof: Load proof Proof not loaded.
L31839
Proof: Load proof Proof not loaded.
End of Section DiadicRationals
Beginning of Section SurrealDiv
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 .
L31861
Proof: Load proof Proof not loaded.
L31883
Proof: Load proof Proof not loaded.
L31929
Proof: Load proof Proof not loaded.
L31975
Proof: Load proof Proof not loaded.
L32020
Proof: Load proof Proof not loaded.
L32065 Definition. We define
SNo_recipauxset to be
λY x X g ⇒ ⋃ y ∈ Y { (1 + (x' + - x ) * y ) * g x' | x' ∈ X } of type
set → set → set → (set → set ) → set .
L32067
Proof: Load proof Proof not loaded.
L32076
Proof: Load proof Proof not loaded.
L32088
Proof: Load proof Proof not loaded.
L32110
Proof: Load proof Proof not loaded.
L32119
Proof: Load proof Proof not loaded.
L32133
Proof: Load proof Proof not loaded.
L32376
Proof: Load proof Proof not loaded.
L32437
Proof: Load proof Proof not loaded.
Beginning of Section recip_SNo_pos
L32529
Proof: Load proof Proof not loaded.
L32554
Proof: Load proof Proof not loaded.
L33177
Proof: Load proof Proof not loaded.
L33182
Proof: Load proof Proof not loaded.
L33187
Proof: Load proof Proof not loaded.
L33212
Proof: Load proof Proof not loaded.
L33235
Proof: Load proof Proof not loaded.
L33256
Proof: Load proof Proof not loaded.
L33262
Proof: Load proof Proof not loaded.
End of Section recip_SNo_pos
L33270
Proof: Load proof Proof not loaded.
L33275
Proof: Load proof Proof not loaded.
L33287
Proof: Load proof Proof not loaded.
L33294
Proof: Load proof Proof not loaded.
L33314
Proof: Load proof Proof not loaded.
L33336
Proof: Load proof Proof not loaded.
L33343
Proof: Load proof Proof not loaded.
L33359
Proof: Load proof Proof not loaded.
L33367
Proof: Load proof Proof not loaded.
Notation . We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo .
L33377
Proof: Load proof Proof not loaded.
L33383
Proof: Load proof Proof not loaded.
L33388
Proof: Load proof Proof not loaded.
L33395
Proof: Load proof Proof not loaded.
L33405
Proof: Load proof Proof not loaded.
L33411
Proof: Load proof Proof not loaded.
L33432
Proof: Load proof Proof not loaded.
L33440
Proof: Load proof Proof not loaded.
L33447
Proof: Load proof Proof not loaded.
L33497
Proof: Load proof Proof not loaded.
L33506
Proof: Load proof Proof not loaded.
L33522
Proof: Load proof Proof not loaded.
L33530
Proof: Load proof Proof not loaded.
L33538
Proof: Load proof Proof not loaded.
L33559
Proof: Load proof Proof not loaded.
L33580
Proof: Load proof Proof not loaded.
L33599
Proof: Load proof Proof not loaded.
L33618
Proof: Load proof Proof not loaded.
End of Section SurrealDiv
Beginning of Section Reals
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 353 and no associativity corresponding to applying term
div_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 .
L33641
Proof: Load proof Proof not loaded.
L33669
Proof: Load proof Proof not loaded.
L33716
Proof: Load proof Proof not loaded.
L33737
Proof: Load proof Proof not loaded.
L33877
Proof: Load proof Proof not loaded.
L33893
Proof: Load proof Proof not loaded.
L33936
Proof: Load proof Proof not loaded.
L33941
Proof: Load proof Proof not loaded.
L33946
Proof: Load proof Proof not loaded.
L34037
Proof: Load proof Proof not loaded.
L34041
Proof: Load proof Proof not loaded.
L34045
Proof: Load proof Proof not loaded.
L34062
Proof: Load proof Proof not loaded.
L34311
Proof: Load proof Proof not loaded.
L34708
Proof: Load proof Proof not loaded.
L34734
Proof: Load proof Proof not loaded.
L34764
Proof: Load proof Proof not loaded.
L34850
Proof: Load proof Proof not loaded.
L34877
Proof: Load proof Proof not loaded.
L35093
Proof: Load proof Proof not loaded.
L35156
Proof: Load proof Proof not loaded.
L35222
Proof: Load proof Proof not loaded.
L35227
Proof: Load proof Proof not loaded.
L35328
Proof: Load proof Proof not loaded.
L35545 Theorem. (
SNo_approx_real_rep )
∀x ∈ real , ∀p : prop , (∀f g ∈ SNoS_ ω ω , (∀n ∈ ω , f n < x ) → (∀n ∈ ω , x < f n + eps_ n ) → (∀n ∈ ω , ∀i ∈ n , f i < f n ) → (∀n ∈ ω , g n + - eps_ n < x ) → (∀n ∈ ω , x < g n ) → (∀n ∈ ω , ∀i ∈ n , g n < g i ) → SNoCutP { f n | n ∈ ω } { g n | n ∈ ω } → x = SNoCut { f n | n ∈ ω } { g n | n ∈ ω } → p ) → p
Proof: Load proof Proof not loaded.
L35728
Proof: Load proof Proof not loaded.
L36204
Proof: Load proof Proof not loaded.
L36255
Proof: Load proof Proof not loaded.
L37620
Proof: Load proof Proof not loaded.
L37678
Proof: Load proof Proof not loaded.
L37757
Proof: Load proof Proof not loaded.
L38122
Proof: Load proof Proof not loaded.
L38866
Proof: Load proof Proof not loaded.
L38872
Proof: Load proof Proof not loaded.
L38898
Proof: Load proof Proof not loaded.
End of Section Reals
Beginning of Section even_odd
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
L38915
Proof: Load proof Proof not loaded.
L38936
Proof: Load proof Proof not loaded.
L38967
Proof: Load proof Proof not loaded.
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 .
L38987
Proof: Load proof Proof not loaded.
End of Section even_odd
Beginning of Section form100_22b
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
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 .
L39036
Proof: Load proof Proof not loaded.
L39203
Proof: Load proof Proof not loaded.
L39256
Proof: Load proof Proof not loaded.
L39285
Proof: Load proof Proof not loaded.
L41035
Proof: Load proof Proof not loaded.
L41048
Proof: Load proof Proof not loaded.
L41056
Proof: Load proof Proof not loaded.
End of Section form100_22b
Beginning of Section rational
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 353 and no associativity corresponding to applying term
div_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 .
End of Section rational
Beginning of Section form100_3
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 353 and no associativity corresponding to applying term
div_SNo .
Notation . We use
^ as an infix operator with priority 342 and which associates to the right corresponding to applying term
exp_SNo_nat .
L41096
Proof: Load proof Proof not loaded.
L41105
Proof: Load proof Proof not loaded.
L41153
Proof: Load proof Proof not loaded.
L41157
Proof: Load proof Proof not loaded.
L41216 Definition. We define
nat_pair to be
λm n ⇒ 2 ^ m * (2 * n + 1 ) of type
set → set → set .
L41218
Proof: Load proof Proof not loaded.
L41230
Proof: Load proof Proof not loaded.
L41439
Proof: Load proof Proof not loaded.
L41476
Proof: Load proof Proof not loaded.
End of Section form100_3
Beginning of Section SurrealSqrt
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 353 and no associativity corresponding to applying term
div_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 .
L41811
Proof: Load proof Proof not loaded.
L41817
Proof: Load proof Proof not loaded.
L41833
Proof: Load proof Proof not loaded.
L41843
Proof: Load proof Proof not loaded.
L41857
Proof: Load proof Proof not loaded.
L41865
Proof: Load proof Proof not loaded.
L41881
Proof: Load proof Proof not loaded.
L41889
Proof: Load proof Proof not loaded.
L41903
Proof: Load proof Proof not loaded.
L41945
Proof: Load proof Proof not loaded.
L41959
Proof: Load proof Proof not loaded.
Beginning of Section sqrt_SNo_nonneg
L42002
Proof: Load proof Proof not loaded.
L42027
Proof: Load proof Proof not loaded.
L42465
Proof: Load proof Proof not loaded.
L42534
Proof: Load proof Proof not loaded.
L42570
Proof: Load proof Proof not loaded.
L42853
Proof: Load proof Proof not loaded.
L43237
Proof: Load proof Proof not loaded.
End of Section sqrt_SNo_nonneg
L43320
Proof: Load proof Proof not loaded.
L43331
Proof: Load proof Proof not loaded.
L43340
Proof: Load proof Proof not loaded.
L43349
Proof: Load proof Proof not loaded.
L43357
Proof: Load proof Proof not loaded.
L43363
Proof: Load proof Proof not loaded.
L43369
Proof: Load proof Proof not loaded.
L43375
Proof: Load proof Proof not loaded.
L43455
Proof: Load proof Proof not loaded.
L43579
Proof: Load proof Proof not loaded.
L43607
Proof: Load proof Proof not loaded.
L43625
Proof: Load proof Proof not loaded.
L43699
Proof: Load proof Proof not loaded.
L43726
Proof: Load proof Proof not loaded.
L43797
Proof: Load proof Proof not loaded.
L44221
Proof: Load proof Proof not loaded.
End of Section SurrealSqrt
Beginning of Section form100_1
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 353 and no associativity corresponding to applying term
div_SNo .
L44647
Proof: Load proof Proof not loaded.
L44684
Proof: Load proof Proof not loaded.
L44847
Proof: Load proof Proof not loaded.
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 353 and no associativity corresponding to applying term
div_SNo .
L44869
Proof: Load proof Proof not loaded.
End of Section form100_1