Primitive . The name
Eps_i is a term of type
(set → prop → set .
Axiom. (
Eps_i_ax ) We take the following as an axiom:
∀P : set → prop ∀x : set , P x P (Eps_i P Definition. We define
True to be
∀p : prop , p → p of type
prop .
Definition. We define
False to be
∀p : prop , p of type
prop .
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 .
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 .
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 .
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
Variable A : SType
Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop Q x y Q y x of type
A → A → prop .
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
Variable A B : SType
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
Variable A : SType
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 .
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 .
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 .
Axiom. (
set_ext ) We take the following as an axiom:
∀X Y : set , X ⊆ Y Y ⊆ X X = Y 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 .
Axiom. (
EmptyAx ) We take the following as an axiom:
Primitive . The name
⋃ is a term of type
set → set .
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 .
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 ).
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 Definition. We define
TransSet to be
λU : set ⇒ ∀x ∈ U , x ⊆ U of type
set → prop .
Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set , X ∈ U ⋃ X ∈ U of type
set → prop .
Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set , X ∈ U 𝒫 X ∈ U of type
set → prop .
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 .
Axiom. (
UnivOf_In ) We take the following as an axiom:
Axiom. (
UnivOf_Min ) We take the following as an axiom:
Theorem. (
andI )
∀A B : prop , A → B → A ∧ B Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
iffI )
∀A B : prop , (A → B → (B → A → (A ↔ B Proof: Load proof Proof not loaded.
Theorem. (
pred_ext )
∀P Q : set → prop (∀x, P x ↔ Q x ) → P = Q Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Theorem. (
PowerI )
∀X Y : set , Y ⊆ X Y ∈ 𝒫 X Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Beginning of Section PropN
Variable P1 P2 P3 : prop
Theorem. (
and3I )
P1 → P2 → P3 → P1 ∧ P2 ∧ P3 Proof: Load proof Proof not loaded.
Theorem. (
and3E )
P1 ∧ P2 ∧ P3 (∀p : prop , (P1 → P2 → P3 → p → p ) Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
or3E )
P1 ∨ P2 ∨ P3 (∀p : prop , (P1 → p → (P2 → p → (P3 → p → p ) Proof: Load proof Proof not loaded.
Variable P4 : prop
Theorem. (
and4I )
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4 Proof: Load proof Proof not loaded.
Variable P5 : prop
Theorem. (
and5I )
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 Proof: Load proof Proof not loaded.
Variable P6 : prop
Theorem. (
and6I )
P1 → P2 → P3 → P4 → P5 → P6 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5 ∧ P6 Proof: Load proof Proof not loaded.
Variable P7 : prop
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
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
iffEL )
∀A B : prop , (A ↔ B → A → B Proof: Load proof Proof not loaded.
Theorem. (
iffER )
∀A B : prop , (A ↔ B → B → A Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
iff_sym )
∀A B : prop , (A ↔ B → (B ↔ A Proof: Load proof Proof not loaded.
Theorem. (
iff_trans )
∀A B C : prop , (A ↔ B → (B ↔ C → (A ↔ C Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
prop_ext_2 )
∀p q : prop , (p → q → (q → p → p = q Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
Subq_tra )
∀X Y Z : set , X ⊆ Y Y ⊆ Z X ⊆ Z Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
UnionI )
∀X x Y : set , x ∈ Y Y ∈ X x ∈ ⋃ X Proof: Load proof Proof not loaded.
Theorem. (
UnionE )
∀X x : set , x ∈ ⋃ X ∃Y : set , x ∈ Y ∧ Y ∈ X Proof: Load proof Proof not loaded.
Theorem. (
UnionE_impred )
∀X x : set , x ∈ ⋃ X ∀p : prop , (∀Y : set , x ∈ Y Y ∈ X p ) → p Proof: Load proof Proof not loaded.
Theorem. (
PowerE )
∀X Y : set , Y ∈ 𝒫 X Y ⊆ X Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
exactly1of2 to be
λA B : prop ⇒ A ∧ ¬ B ∨ ¬ A ∧ B of type
prop → prop → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
ReplI )
∀A : set , ∀F : set → set ∀x : set , x ∈ A F x ∈ { F x | x ∈ A } Proof: Load proof Proof not loaded.
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.
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.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
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.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Notation .
{x ,y } is notation for
UPair x y .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
Sing to be
λx ⇒ { x , x } of type
set → set .
Notation .
{x } is notation for
Sing x .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
binunionE' )
∀X Y z, ∀p : prop , (z ∈ X p → (z ∈ Y p → (z ∈ X ∪ Y p Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
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 .
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.
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.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
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 ).
Theorem. (
SepI )
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ X P x x ∈ { x ∈ X | P x } Proof: Load proof Proof not loaded.
Theorem. (
SepE )
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X ∧ P x Proof: Load proof Proof not loaded.
Theorem. (
SepE1 )
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } x ∈ X Proof: Load proof Proof not loaded.
Theorem. (
SepE2 )
∀X : set , ∀P : (set → prop , ∀x : set , x ∈ { x ∈ X | P x } P x Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 ).
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.
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.
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.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
ordsucc to be
λx : set ⇒ x ∪ { x } of type
set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
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.
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.
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 .
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.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
Proof: Load proof Proof not loaded.
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 .
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.
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.
Proof: Load proof Proof not loaded.
Definition. We define
atleastp to be
λX Y : set ⇒ ∃f : set → set inj X Y f of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
equip to be
λX Y : set ⇒ ∃f : set → set bij X Y f of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Beginning of Section SchroederBernstein
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section SchroederBernstein
Beginning of Section PigeonHole
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section PigeonHole
Proof: Load proof Proof not loaded.
Theorem. (
cases_1 )
∀i ∈ 1 ∀p : set → prop p 0 p i Proof: Load proof Proof not loaded.
Theorem. (
cases_2 )
∀i ∈ 2 ∀p : set → prop p 0 p 1 p i Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
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.
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.
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
Variable P : (set → set → prop
Definition. We define
Descr_ii to be
λx : set ⇒ Eps_i (λy ⇒ ∀h : set → set P h h x = y ) of type
set → set .
Hypothesis Pex : ∃f : set → set P f Hypothesis Puniq : ∀f g : set → set P f P g f = g
Proof: Load proof Proof not loaded.
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set → prop
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 .
Hypothesis Pex : ∃f : set → set → set P f Hypothesis Puniq : ∀f g : set → set → set P f P g f = g
Proof: Load proof Proof not loaded.
End of Section Descr_iii
Beginning of Section Descr_Vo1
Definition. We define
Descr_Vo1 to be
λx : set ⇒ ∀h : set → prop P h h x of type
Vo 1 .
Hypothesis Pex : ∃f : Vo 1 P f Hypothesis Puniq : ∀f g : Vo 1 P f P g f = g
Proof: Load proof Proof not loaded.
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
Definition. We define
If_ii to be
λx ⇒ if p then f x else g x of type
set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
Definition. We define
If_iii to be
λx y ⇒ if p then f x y else g x y of type
set → set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set → set
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Hypothesis Fr : ∀X : set , ∀g h : set → set (∀x ∈ X , g x = h x ) → F X g = F X h
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set → (set → set
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set (∀x ∈ X , g x = h x ) → F X g = F X h
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set → (set → (set → set → set → (set → set → set
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set → set (∀x ∈ X , g x = h x ) → F X g = F X h
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : set → set → set
Let F : set → (set → set → set λn g ⇒ if ⋃ n ∈ n then f (⋃ n (g (⋃ n else z 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.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
Pi_nat to be
λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i ) n of type
(set → set → set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section form100_52
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
finite to be
λX ⇒ ∃n ∈ ω equip X n of type
set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Definition. We define
divides_nat to be
λm n ⇒ m ∈ ω ∧ n ∈ ω ∧ ∃k ∈ ω m * k = n of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section InfiniteRamsey
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
Inj0 to be
λX ⇒ { Inj1 x | x ∈ X } of type
set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Beginning of Section pair_setsum
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
pairI0 )
∀X Y x, x ∈ X pair 0 x ∈ pair X Y Proof: Load proof Proof not loaded.
Theorem. (
pairI1 )
∀X Y y, y ∈ Y pair 1 y ∈ pair X Y Proof: Load proof Proof not loaded.
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.
Theorem. (
pairE0 )
∀X Y x, pair 0 x ∈ pair X Y x ∈ X Proof: Load proof Proof not loaded.
Theorem. (
pairE1 )
∀X Y y, pair 1 y ∈ pair X Y y ∈ Y Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
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.
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.
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 .
Let lam : set → (set → set → set Sigma 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 .
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.
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.
Theorem. (
apI )
∀f x y, pair x y ∈ f y ∈ f x Proof: Load proof Proof not loaded.
Theorem. (
apE )
∀f x y, y ∈ f x pair x y ∈ f Proof: Load proof Proof not loaded.
Theorem. (
beta )
∀X : set , ∀F : set → set ∀x : set , x ∈ X (λ x ∈ X ⇒ F x x = F x Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Theorem. (
ap0_Sigma )
∀X : set , ∀Y : set → set ∀z : set , z ∈ (∑ x ∈ X , Y x (z 0 ∈ X Proof: Load proof Proof not loaded.
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.
Definition. We define
pair_p to be
λu : set ⇒ pair (u 0 (u 1 = u of type
set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
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.
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.
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.
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 .
Proof: Load proof Proof not loaded.
Beginning of Section Tuples
Variable x0 x1 : set
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section Tuples
Proof: Load proof Proof not loaded.
Theorem. (
lamI2 )
∀X, ∀F : set → set ∀x ∈ X , ∀y ∈ F x ( x ,y ) ∈ λ x ∈ X ⇒ F x Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
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 .
Proof: Load proof Proof not loaded.
Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀beta ∈ alpha , p beta ↔ q beta of type
set → (set → prop → (set → prop → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
SNoElts_ to be
λalpha ⇒ alpha ∪ { beta ' | beta ∈ alpha } of type
set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
SNo to be
λx ⇒ ∃alpha, ordinal alpha ∧ SNo_ alpha x of type
set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) of type
set → set → set → prop .
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section TaggedSets2
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Beginning of Section SurrealRecI
Variable F : set → (set → set → set
Hypothesis Fr : ∀z, SNo z ∀g h : set → set (∀w ∈ SNoS_ (SNoLev z g w = h w ) → F z g = F z h
Proof: Load proof Proof not loaded.
End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set → (set → set
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 ) Hypothesis Fr : ∀z, SNo z ∀g h : set → (set → set (∀w ∈ SNoS_ (SNoLev z g w = h w ) → F z g = F z h
Proof: Load proof Proof not loaded.
End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set → set
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 )
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section SurrealRec2
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
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.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Beginning of Section mul_SNo_assoc_lems
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 .
Hypothesis SNo_M : ∀x y, SNo x SNo y SNo (x * y Hypothesis DL : ∀x y z, SNo x SNo y SNo z x * (y + z = x * y + x * z Hypothesis DR : ∀x y z, SNo x SNo y SNo z (x + y * z = x * z + y * z 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 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 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.
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
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Definition. We define
int to be
ω ∪ { - n | n ∈ ω } of type
set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
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 .
Proof: Load proof Proof not loaded.
Definition. We define
Pi_SNo to be
λf n ⇒ nat_primrec 1 (λi r ⇒ r * f i ) n of type
(set → set → set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Definition. We define
SNo_max_of to be
λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X , SNo y y ≤ x of type
set → set → prop .
Definition. We define
SNo_min_of to be
λX x ⇒ x ∈ X ∧ SNo x ∧ ∀y ∈ X , SNo y x ≤ y of type
set → set → prop .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Beginning of Section recip_SNo_pos
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section recip_SNo_pos
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Definition. We define
nat_pair to be
λm n ⇒ 2 ^ m * (2 * n + 1 of type
set → set → set .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Beginning of Section sqrt_SNo_nonneg
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
End of Section sqrt_SNo_nonneg
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
Proof: Load proof Proof not loaded.
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 .
Proof: Load proof Proof not loaded.
End of Section form100_1