Primitive. The name
Eps_i is a term of type
(set → prop) → set.
L2Axiom. (
Eps_i_ax) We take the following as an axiom:
∀P : set → prop, ∀x : set, P x → P (Eps_i P)
L4Definition. We define
True to be
∀p : prop, p → p of type
prop.
L6Definition. We define
False to be
∀p : prop, p of type
prop.
L7Definition. 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.
L11Definition. 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.
L15Definition. 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.
L19Definition. 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
L26Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop, Q x y → Q y x of type
A → A → prop.
L27Definition. 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
L35Axiom. (
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
L40Definition. 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
exists x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex.
L44Axiom. (
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.
L48Definition. 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.
L50Axiom. (
set_ext) We take the following as an axiom:
∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y
L52Axiom. (
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
exists 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.
L58Axiom. (
EmptyAx) We take the following as an axiom:
Primitive. The name
Union is a term of type
set → set.
L61Axiom. (
UnionEq) We take the following as an axiom:
Primitive. The name
Power is a term of type
set → set.
L65Axiom. (
PowerEq) We take the following as an axiom:
Primitive. The name
Repl is a term of type
set → (set → set) → set.
Notation.
{B| x ∈ A} is notation for
Repl A (λ x . B).
L70Axiom. (
ReplEq) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} <-> exists x ∈ A, y = F x
L72Definition. We define
TransSet to be
λU : set ⇒ ∀x ∈ U, x ⊆ U of type
set → prop.
L74Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set, X ∈ U → Union X ∈ U of type
set → prop.
L76Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set, X ∈ U → Power X ∈ U of type
set → prop.
L77Definition. 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.
L85Axiom. (
UnivOf_In) We take the following as an axiom:
L91Axiom. (
UnivOf_Min) We take the following as an axiom:
L96Axiom. (
FalseE) We take the following as an axiom:
L98Axiom. (
TrueI) We take the following as an axiom:
L100Axiom. (
andI) We take the following as an axiom:
∀A B : prop, A → B → A /\ B
L102Axiom. (
andEL) We take the following as an axiom:
L104Axiom. (
andER) We take the following as an axiom:
L106Axiom. (
orIL) We take the following as an axiom:
L108Axiom. (
orIR) We take the following as an axiom:
Beginning of Section PropN
L112Variable P1 P2 P3 : prop
L114Axiom. (
and3I) We take the following as an axiom:
P1 → P2 → P3 → P1 /\ P2 /\ P3
L116Axiom. (
and3E) We take the following as an axiom:
P1 /\ P2 /\ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
L118Axiom. (
or3I1) We take the following as an axiom:
L120Axiom. (
or3I2) We take the following as an axiom:
L122Axiom. (
or3I3) We take the following as an axiom:
L124Axiom. (
or3E) We take the following as an axiom:
P1 \/ P2 \/ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)
L128Axiom. (
and4I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 /\ P2 /\ P3 /\ P4
L132Axiom. (
and5I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 /\ P2 /\ P3 /\ P4 /\ P5
End of Section PropN
L140Axiom. (
iffI) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → (A <-> B)
L142Axiom. (
iffEL) We take the following as an axiom:
∀A B : prop, (A <-> B) → A → B
L144Axiom. (
iffER) We take the following as an axiom:
∀A B : prop, (A <-> B) → B → A
L146Axiom. (
iff_refl) We take the following as an axiom:
L148Axiom. (
iff_sym) We take the following as an axiom:
∀A B : prop, (A <-> B) → (B <-> A)
L150Axiom. (
iff_trans) We take the following as an axiom:
∀A B C : prop, (A <-> B) → (B <-> C) → (A <-> C)
L152Axiom. (
eq_i_tra) We take the following as an axiom:
∀x y z, x = y → y = z → x = z
L154Axiom. (
f_eq_i) We take the following as an axiom:
∀f : set → set, ∀x y, x = y → f x = f y
L156Axiom. (
neq_i_sym) We take the following as an axiom:
L158Definition. We define
nIn to be
λx X ⇒ ~ In x X of type
set → set → prop.
Notation. We use
/:e as an infix operator with priority 502 and no associativity corresponding to applying term
nIn.
L163Axiom. (
Eps_i_ex) We take the following as an axiom:
∀P : set → prop, (exists x, P x) → P (Eps_i P)
L165Axiom. (
pred_ext) We take the following as an axiom:
∀P Q : set → prop, (∀x, P x <-> Q x) → P = Q
L167Axiom. (
prop_ext_2) We take the following as an axiom:
∀p q : prop, (p → q) → (q → p) → p = q
L169Axiom. (
Subq_ref) We take the following as an axiom:
L171Axiom. (
Subq_tra) We take the following as an axiom:
∀X Y Z : set, X ⊆ Y → Y ⊆ Z → X ⊆ Z
L173Axiom. (
Subq_contra) We take the following as an axiom:
∀X Y z : set, X ⊆ Y → z /:e Y → z /:e X
L175Axiom. (
EmptyE) We take the following as an axiom:
L177Axiom. (
Subq_Empty) We take the following as an axiom:
L181Axiom. (
Empty_eq) We take the following as an axiom:
L183Axiom. (
UnionI) We take the following as an axiom:
∀X x Y : set, x ∈ Y → Y ∈ X → x ∈ Union X
L185Axiom. (
UnionE) We take the following as an axiom:
∀X x : set, x ∈ Union X → exists Y : set, x ∈ Y /\ Y ∈ X
L187Axiom. (
UnionE_impred) We take the following as an axiom:
∀X x : set, x ∈ Union X → ∀p : prop, (∀Y : set, x ∈ Y → Y ∈ X → p) → p
L189Axiom. (
PowerI) We take the following as an axiom:
L191Axiom. (
PowerE) We take the following as an axiom:
L197Axiom. (
xm) We take the following as an axiom:
L199Axiom. (
dneg) We take the following as an axiom:
L203Axiom. (
eq_or_nand) We take the following as an axiom:
Primitive. The name
exactly1of2 is a term of type
prop → prop → prop.
L212Axiom. (
exactly1of2_E) We take the following as an axiom:
∀A B : prop, exactly1of2 A B → ∀p : prop, (A → ~ B → p) → (~ A → B → p) → p
L220Axiom. (
ReplI) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}
L222Axiom. (
ReplE) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → exists x ∈ A, y = F x
L224Axiom. (
ReplE_impred) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∀p : prop, (∀x : set, x ∈ A → y = F x → p) → p
L226Axiom. (
ReplE') We take the following as an axiom:
∀X, ∀f : set → set, ∀p : set → prop, (∀x ∈ X, p (f x)) → ∀y ∈ {f x|x ∈ X}, p y
L228Axiom. (
Repl_Empty) We take the following as an axiom:
L230Axiom. (
ReplEq_ext_sub) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} ⊆ {G x|x ∈ X}
L232Axiom. (
ReplEq_ext) We take the following as an axiom:
∀X, ∀F G : set → set, (∀x ∈ X, F x = G x) → {F x|x ∈ X} = {G x|x ∈ X}
L234Axiom. (
Repl_inv_eq) We take the following as an axiom:
∀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
L238Axiom. (
Repl_invol_eq) We take the following as an axiom:
∀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
Primitive. The name
If_i is a term 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.
L250Axiom. (
If_i_0) We take the following as an axiom:
L253Axiom. (
If_i_1) We take the following as an axiom:
L256Axiom. (
If_i_or) We take the following as an axiom:
Primitive. The name
UPair is a term of type
set → set → set.
Notation.
{x,y} is notation for
UPair x y.
L263Axiom. (
UPairE) We take the following as an axiom:
∀x y z : set, x ∈ {y,z} → x = y \/ x = z
L266Axiom. (
UPairI1) We take the following as an axiom:
L268Axiom. (
UPairI2) We take the following as an axiom:
Primitive. The name
Sing is a term of type
set → set.
Notation.
{x} is notation for
Sing x.
L274Axiom. (
SingI) We take the following as an axiom:
L276Axiom. (
SingE) We take the following as an axiom:
∀x y : set, y ∈ {x} → y = x
L278Axiom. (
Sing_inj) We take the following as an axiom:
Primitive. The name
binunion is a term 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.
L285Axiom. (
binunionI1) We take the following as an axiom:
∀X Y z : set, z ∈ X → z ∈ X :\/: Y
L287Axiom. (
binunionI2) We take the following as an axiom:
∀X Y z : set, z ∈ Y → z ∈ X :\/: Y
L289Axiom. (
binunionE) We take the following as an axiom:
L291Axiom. (
binunionE') We take the following as an axiom:
∀X Y z, ∀p : prop, (z ∈ X → p) → (z ∈ Y → p) → (z ∈ X :\/: Y → p)
L311Definition. 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.
Primitive. The name
famunion is a term 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.
L320Axiom. (
famunionI) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ F x → y ∈ \/_ x ∈ X, F x
L322Axiom. (
famunionE) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (\/_ x ∈ X, F x) → exists x ∈ X, y ∈ F x
L324Axiom. (
famunionE_impred) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (\/_ x ∈ X, F x) → ∀p : prop, (∀x, x ∈ X → y ∈ F x → p) → p
Beginning of Section SepSec
L336Variable P : set → prop
Primitive. The name
Sep is a term of type
set.
End of Section SepSec
Notation.
{x ∈ A | B} is notation for
Sep A (λ x . B).
L346Axiom. (
SepI) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}
L348Axiom. (
SepE) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X /\ P x
L350Axiom. (
SepE1) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
L352Axiom. (
SepE2) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
L354Axiom. (
Sep_Empty) We take the following as an axiom:
L356Axiom. (
Sep_Subq) We take the following as an axiom:
∀X : set, ∀P : set → prop, {x ∈ X|P x} ⊆ X
Primitive. The name
ReplSep is a term of type
set → (set → prop) → (set → set) → set.
Notation.
{B| x ∈ A, C} is notation for
ReplSep A (λ x . C) (λ x . B).
L364Axiom. (
ReplSepI) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀F : set → set, ∀x : set, x ∈ X → P x → F x ∈ {F x|x ∈ X, P x}
L366Axiom. (
ReplSepE) We take the following as an axiom:
∀X : set, ∀P : set → prop, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ X, P x} → exists x : set, x ∈ X /\ P x /\ y = F x
L368Axiom. (
ReplSepE_impred) We take the following as an axiom:
∀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
Primitive. The name
binintersect is a term 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.
Primitive. The name
setminus is a term of type
set → set → set.
Notation. We use
:\: as an infix operator with priority 350 and no associativity corresponding to applying term
setminus.
L400Axiom. (
setminusI) We take the following as an axiom:
∀X Y z, (z ∈ X) → (z /:e Y) → z ∈ X :\: Y
L402Axiom. (
setminusE) We take the following as an axiom:
L404Axiom. (
setminusE1) We take the following as an axiom:
∀X Y z, (z ∈ X :\: Y) → z ∈ X
L406Axiom. (
setminusE2) We take the following as an axiom:
L416Axiom. (
In_irref) We take the following as an axiom:
L418Axiom. (
In_no2cycle) We take the following as an axiom:
Primitive. The name
ordsucc is a term of type
set → set.
L423Axiom. (
ordsuccI1) We take the following as an axiom:
L425Axiom. (
ordsuccI2) We take the following as an axiom:
L427Axiom. (
ordsuccE) We take the following as an axiom:
Notation. Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc.
L435Axiom. (
ordsucc_inj) We take the following as an axiom:
L439Axiom. (
In_0_1) We take the following as an axiom:
L441Axiom. (
In_0_2) We take the following as an axiom:
L443Axiom. (
In_1_2) We take the following as an axiom:
L445Axiom. (
In_1_3) We take the following as an axiom:
L447Axiom. (
In_2_3) We take the following as an axiom:
L449Axiom. (
In_1_4) We take the following as an axiom:
L451Axiom. (
In_2_4) We take the following as an axiom:
L453Axiom. (
In_3_4) We take the following as an axiom:
L455Axiom. (
In_1_5) We take the following as an axiom:
L457Axiom. (
In_2_5) We take the following as an axiom:
L459Axiom. (
In_3_5) We take the following as an axiom:
L461Axiom. (
In_4_5) We take the following as an axiom:
L463Axiom. (
In_1_6) We take the following as an axiom:
L465Axiom. (
In_1_7) We take the following as an axiom:
L467Axiom. (
In_1_8) We take the following as an axiom:
L469Definition. 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.
L471Axiom. (
nat_0) We take the following as an axiom:
L473Axiom. (
nat_ordsucc) We take the following as an axiom:
L475Axiom. (
nat_1) We take the following as an axiom:
L477Axiom. (
nat_2) We take the following as an axiom:
L479Axiom. (
nat_3) We take the following as an axiom:
L481Axiom. (
nat_4) We take the following as an axiom:
L483Axiom. (
nat_5) We take the following as an axiom:
L485Axiom. (
nat_6) We take the following as an axiom:
L487Axiom. (
nat_7) We take the following as an axiom:
L489Axiom. (
nat_8) We take the following as an axiom:
L495Axiom. (
nat_ind) We take the following as an axiom:
L499Axiom. (
nat_inv) We take the following as an axiom:
L503Axiom. (
nat_p_trans) We take the following as an axiom:
L505Axiom. (
nat_trans) We take the following as an axiom:
L511Axiom. (
cases_1) We take the following as an axiom:
∀i ∈ 1, ∀p : set → prop, p 0 → p i
L513Axiom. (
cases_2) We take the following as an axiom:
∀i ∈ 2, ∀p : set → prop, p 0 → p 1 → p i
L515Axiom. (
cases_3) We take the following as an axiom:
∀i ∈ 3, ∀p : set → prop, p 0 → p 1 → p 2 → p i
L517Axiom. (
neq_0_1) We take the following as an axiom:
L519Axiom. (
neq_1_0) We take the following as an axiom:
L521Axiom. (
neq_0_2) We take the following as an axiom:
L523Axiom. (
neq_2_0) We take the following as an axiom:
L525Axiom. (
neq_1_2) We take the following as an axiom:
L527Axiom. (
neq_1_3) We take the following as an axiom:
L529Axiom. (
neq_2_3) We take the following as an axiom:
L531Axiom. (
neq_2_4) We take the following as an axiom:
L533Axiom. (
neq_3_4) We take the following as an axiom:
L535Axiom. (
ZF_closed_E) We take the following as an axiom:
Primitive. The name
omega is a term of type
set.
L568Axiom. (
omega_nat_p) We take the following as an axiom:
L570Axiom. (
nat_p_omega) We take the following as an axiom:
L588Axiom. (
ordinal_1) We take the following as an axiom:
L590Axiom. (
ordinal_2) We take the following as an axiom:
L622Axiom. (
ordinal_ind) We take the following as an axiom:
∀p : set → prop, (∀alpha, ordinal alpha → (∀beta ∈ alpha, p beta) → p alpha) → ∀alpha, ordinal alpha → p alpha
L629Definition. 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.
L635Definition. We define
bij to be
λX Y f ⇒ (∀u ∈ X, f u ∈ Y) /\ (∀u v ∈ X, f u = f v → u = v) /\ (∀w ∈ Y, exists u ∈ X, f u = w) of type
set → set → (set → set) → prop.
L643Axiom. (
bijI) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀u ∈ X, f u ∈ Y) → (∀u v ∈ X, f u = f v → u = v) → (∀w ∈ Y, exists u ∈ X, f u = w) → bij X Y f
L649Axiom. (
bijE) We take the following as an axiom:
∀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, exists u ∈ X, f u = w) → p) → p
Primitive. The name
inv is a term of type
set → (set → set) → set → set.
L661Axiom. (
surj_rinv) We take the following as an axiom:
∀X Y, ∀f : set → set, (∀w ∈ Y, exists u ∈ X, f u = w) → ∀y ∈ Y, inv X f y ∈ X /\ f (inv X f y) = y
L663Axiom. (
inj_linv) We take the following as an axiom:
∀X, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x
L665Axiom. (
bij_inv) We take the following as an axiom:
∀X Y, ∀f : set → set, bij X Y f → bij Y X (inv X f)
L667Axiom. (
bij_id) We take the following as an axiom:
L669Axiom. (
bij_comp) We take the following as an axiom:
∀X Y Z : set, ∀f g : set → set, bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x))
L671Definition. We define
equip to be
λX Y : set ⇒ exists f : set → set, bij X Y f of type
set → set → prop.
L674Axiom. (
equip_ref) We take the following as an axiom:
L676Axiom. (
equip_sym) We take the following as an axiom:
L678Axiom. (
equip_tra) We take the following as an axiom:
Beginning of Section SchroederBernstein
End of Section SchroederBernstein
Beginning of Section PigeonHole
End of Section PigeonHole
L707Definition. We define
finite to be
λX ⇒ exists n ∈ omega, equip X n of type
set → prop.
L709Axiom. (
finite_ind) We take the following as an axiom:
L722Axiom. (
Subq_finite) We take the following as an axiom:
L726Axiom. (
exandE_i) We take the following as an axiom:
∀P Q : set → prop, (exists x, P x /\ Q x) → ∀r : prop, (∀x, P x → Q x → r) → r
L728Axiom. (
exandE_ii) We take the following as an axiom:
∀P Q : (set → set) → prop, (exists x : set → set, P x /\ Q x) → ∀p : prop, (∀x : set → set, P x → Q x → p) → p
L730Axiom. (
exandE_iii) We take the following as an axiom:
∀P Q : (set → set → set) → prop, (exists x : set → set → set, P x /\ Q x) → ∀p : prop, (∀x : set → set → set, P x → Q x → p) → p
L732Axiom. (
exandE_iiii) We take the following as an axiom:
∀P Q : (set → set → set → set) → prop, (exists x : set → set → set → set, P x /\ Q x) → ∀p : prop, (∀x : set → set → set → set, P x → Q x → p) → p
Beginning of Section Descr_ii
L736Variable P : (set → set) → prop
Primitive. The name
Descr_ii is a term of type
set → set.
L741Hypothesis Pex : exists f : set → set, P f
L743Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g
End of Section Descr_ii
Beginning of Section Descr_iii
L750Variable P : (set → set → set) → prop
Primitive. The name
Descr_iii is a term of type
set → set → set.
L755Hypothesis Pex : exists f : set → set → set, P f
L757Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g
End of Section Descr_iii
Beginning of Section Descr_Vo1
Primitive. The name
Descr_Vo1 is a term of type
Vo 1.
L769Hypothesis Pex : exists f : Vo 1, P f
L771Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g
End of Section Descr_Vo1
Beginning of Section If_ii
L780Variable f g : set → set
Primitive. The name
If_ii is a term of type
set → set.
L784Axiom. (
If_ii_1) We take the following as an axiom:
L786Axiom. (
If_ii_0) We take the following as an axiom:
End of Section If_ii
Beginning of Section If_iii
L794Variable f g : set → set → set
Primitive. The name
If_iii is a term of type
set → set → set.
L798Axiom. (
If_iii_1) We take the following as an axiom:
L800Axiom. (
If_iii_0) We take the following as an axiom:
End of Section If_iii
Beginning of Section EpsilonRec_i
L806Variable F : set → (set → set) → set
L808Definition. 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.
Primitive. The name
In_rec_i is a term of type
set → set.
L821Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
L829Axiom. (
In_rec_i_eq) We take the following as an axiom:
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
L835Variable F : set → (set → (set → set)) → (set → set)
L837Definition. 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.
Primitive. The name
In_rec_ii is a term of type
set → (set → set).
L850Hypothesis Fr : ∀X : set, ∀g h : set → (set → set), (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
L864Variable F : set → (set → (set → set → set)) → (set → set → set)
L866Definition. 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.
Primitive. The name
In_rec_iii is a term of type
set → (set → set → set).
L879Hypothesis Fr : ∀X : set, ∀g h : set → (set → set → set), (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_iii
Beginning of Section NatRec
L895Variable f : set → set → set
L899Axiom. (
nat_primrec_r) We take the following as an axiom:
∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
End of Section NatRec
Beginning of Section NatArith
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat.
L913Axiom. (
add_nat_0R) We take the following as an axiom:
L915Axiom. (
add_nat_SR) We take the following as an axiom:
L917Axiom. (
add_nat_p) We take the following as an axiom:
L921Axiom. (
add_nat_0L) We take the following as an axiom:
L923Axiom. (
add_nat_SL) We take the following as an axiom:
L925Axiom. (
add_nat_com) We take the following as an axiom:
L929Definition. 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.
L933Axiom. (
mul_nat_0R) We take the following as an axiom:
L935Axiom. (
mul_nat_SR) We take the following as an axiom:
L937Axiom. (
mul_nat_p) We take the following as an axiom:
End of Section NatArith
L944Axiom. (
Inj1_eq) We take the following as an axiom:
L946Axiom. (
Inj1I1) We take the following as an axiom:
L948Axiom. (
Inj1I2) We take the following as an axiom:
L950Axiom. (
Inj1E) We take the following as an axiom:
L952Axiom. (
Inj1NE1) We take the following as an axiom:
L954Axiom. (
Inj1NE2) We take the following as an axiom:
L956Definition. We define
Inj0 to be
λX ⇒ {Inj1 x|x ∈ X} of type
set → set.
L959Axiom. (
Inj0I) We take the following as an axiom:
L961Axiom. (
Inj0E) We take the following as an axiom:
L966Axiom. (
Unj_eq) We take the following as an axiom:
L968Axiom. (
Unj_Inj1_eq) We take the following as an axiom:
L970Axiom. (
Inj1_inj) We take the following as an axiom:
L972Axiom. (
Unj_Inj0_eq) We take the following as an axiom:
L974Axiom. (
Inj0_inj) We take the following as an axiom:
L976Axiom. (
Inj0_0) We take the following as an axiom:
Notation. We use
:+: as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum.
L985Axiom. (
Inj0_setsum) We take the following as an axiom:
L987Axiom. (
Inj1_setsum) We take the following as an axiom:
L997Axiom. (
eq_1_Sing0) We take the following as an axiom:
L1003Axiom. (
setsum_0_0) We take the following as an axiom:
Beginning of Section pair_setsum
L1013Definition. We define
proj0 to be
λZ ⇒ {Unj z|z ∈ Z, exists x : set, Inj0 x = z} of type
set → set.
L1015Definition. We define
proj1 to be
λZ ⇒ {Unj z|z ∈ Z, exists y : set, Inj1 y = z} of type
set → set.
L1020Axiom. (
pairI0) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
L1022Axiom. (
pairI1) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
L1024Axiom. (
pairE) We take the following as an axiom:
∀X Y z, z ∈ pair X Y → (exists x ∈ X, z = pair 0 x) \/ (exists y ∈ Y, z = pair 1 y)
L1026Axiom. (
pairE0) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
L1028Axiom. (
pairE1) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
L1030Axiom. (
proj0I) We take the following as an axiom:
L1032Axiom. (
proj0E) We take the following as an axiom:
L1034Axiom. (
proj1I) We take the following as an axiom:
L1036Axiom. (
proj1E) We take the following as an axiom:
L1042Definition. We define
Sigma to be
λX Y ⇒ \/_ x ∈ X, {pair x y|y ∈ Y x} of type
set → (set → set) → set.
Notation. We use
Sigma_ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma.
L1049Axiom. (
pair_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ Sigma_ x ∈ X, Y x
L1055Axiom. (
proj0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (Sigma_ x ∈ X, Y x) → proj0 z ∈ X
L1057Axiom. (
proj1_Sigma) We take the following as an axiom:
L1059Axiom. (
pair_Sigma_E1) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (Sigma_ x ∈ X, Y x) → y ∈ Y x
L1061Axiom. (
Sigma_E) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (Sigma_ x ∈ X, Y x) → exists x ∈ X, exists y ∈ Y x, z = pair x y
L1063Definition. We define
setprod to be
λX Y : set ⇒ Sigma_ 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.
L1067Let lam : set → (set → set) → set ≝ Sigma
L1070Definition. We define
ap to be
λf x ⇒ {proj1 z|z ∈ f, exists 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.
L1076Axiom. (
lamI) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, pair x y ∈ λx ∈ X ⇒ F x
L1078Axiom. (
lamE) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → exists x ∈ X, exists y ∈ F x, z = pair x y
L1080Axiom. (
apI) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
L1082Axiom. (
apE) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
L1084Axiom. (
beta) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x
L1086Axiom. (
proj0_ap_0) We take the following as an axiom:
L1088Axiom. (
proj1_ap_1) We take the following as an axiom:
L1090Axiom. (
pair_ap_0) We take the following as an axiom:
∀x y : set, (pair x y) 0 = x
L1092Axiom. (
pair_ap_1) We take the following as an axiom:
∀x y : set, (pair x y) 1 = y
L1094Axiom. (
ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (Sigma_ x ∈ X, Y x) → (z 0) ∈ X
L1096Axiom. (
ap1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (Sigma_ x ∈ X, Y x) → (z 1) ∈ (Y (z 0))
L1098Definition. We define
pair_p to be
λu : set ⇒ pair (u 0) (u 1) = u of type
set → prop.
L1101Axiom. (
pair_p_I) We take the following as an axiom:
L1105Axiom. (
tuple_pair) We take the following as an axiom:
∀x y : set, pair x y = (x,y)
L1107Definition. We define
Pi to be
λX Y ⇒ {f ∈ Power (Sigma_ x ∈ X, Union (Y x))|∀x ∈ X, f x ∈ Y x} of type
set → (set → set) → set.
Notation. We use
Pi_ x...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi.
L1111Axiom. (
PiI) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, (∀u ∈ f, pair_p u /\ u 0 ∈ X) → (∀x ∈ X, f x ∈ Y x) → f ∈ Pi_ x ∈ X, Y x
L1114Axiom. (
lam_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀F : set → set, (∀x ∈ X, F x ∈ Y x) → (λx ∈ X ⇒ F x) ∈ (Pi_ x ∈ X, Y x)
L1117Axiom. (
ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (Pi_ x ∈ X, Y x) → x ∈ X → f x ∈ Y x
L1119Definition. We define
setexp to be
λX Y : set ⇒ Pi_ 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.
L1125Axiom. (
lamI2) We take the following as an axiom:
∀X, ∀F : set → set, ∀x ∈ X, ∀y ∈ F x, (x,y) ∈ λx ∈ X ⇒ F x
Beginning of Section Tuples
L1129Variable x0 x1 : set
End of Section Tuples
L1139Axiom. (
tuple_2_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, (x,y) ∈ Sigma_ x ∈ X, Y x
End of Section pair_setsum
Primitive. The name
DescrR_i_io_1 is a term of type
(set → (set → prop) → prop) → set.
Primitive. The name
DescrR_i_io_2 is a term of type
(set → (set → prop) → prop) → set → prop.
L1155Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀beta ∈ alpha, p beta <-> q beta of type
set → (set → prop) → (set → prop) → prop.
L1162Axiom. (
PNoEq_ref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p p
L1164Axiom. (
PNoEq_sym_) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoEq_ alpha q p
L1166Axiom. (
PNoEq_tra_) We take the following as an axiom:
L1170Definition. We define
PNoLt_ to be
λalpha p q ⇒ exists beta ∈ alpha, PNoEq_ beta p q /\ ~ p beta /\ q beta of type
set → (set → prop) → (set → prop) → prop.
L1173Axiom. (
PNoLt_E_) We take the following as an axiom:
L1176Axiom. (
PNoLt_irref_) We take the following as an axiom:
∀alpha, ∀p : set → prop, ~ PNoLt_ alpha p p
L1178Axiom. (
PNoLt_mon_) We take the following as an axiom:
L1183Axiom. (
PNoLt_tra_) We take the following as an axiom:
Primitive. The name
PNoLt is a term of type
set → (set → prop) → set → (set → prop) → prop.
L1188Axiom. (
PNoLtI1) We take the following as an axiom:
L1191Axiom. (
PNoLtI2) We take the following as an axiom:
L1194Axiom. (
PNoLtI3) We take the following as an axiom:
L1197Axiom. (
PNoLtE) We take the following as an axiom:
L1205Axiom. (
PNoLt_irref) We take the following as an axiom:
∀alpha, ∀p : set → prop, ~ PNoLt alpha p alpha p
L1211Axiom. (
PNoLtEq_tra) We take the following as an axiom:
L1213Axiom. (
PNoEqLt_tra) We take the following as an axiom:
L1215Axiom. (
PNoLt_tra) We take the following as an axiom:
L1217Definition. 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.
L1220Axiom. (
PNoLeI1) We take the following as an axiom:
L1223Axiom. (
PNoLeI2) We take the following as an axiom:
∀alpha, ∀p q : set → prop, PNoEq_ alpha p q → PNoLe alpha p alpha q
L1226Axiom. (
PNoLe_ref) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoLe alpha p alpha p
L1232Axiom. (
PNoLtLe_tra) We take the following as an axiom:
L1234Axiom. (
PNoLeLt_tra) We take the following as an axiom:
L1236Axiom. (
PNoEqLe_tra) We take the following as an axiom:
L1238Axiom. (
PNoLe_tra) We take the following as an axiom:
L1240Definition. We define
PNo_downc to be
λL alpha p ⇒ exists beta, ordinal beta /\ exists q : set → prop, L beta q /\ PNoLe alpha p beta q of type
(set → (set → prop) → prop) → set → (set → prop) → prop.
L1243Definition. We define
PNo_upc to be
λR alpha p ⇒ exists beta, ordinal beta /\ exists q : set → prop, R beta q /\ PNoLe beta q alpha p of type
(set → (set → prop) → prop) → set → (set → prop) → prop.
L1246Axiom. (
PNoLe_downc) We take the following as an axiom:
L1250Axiom. (
PNo_downc_ref) We take the following as an axiom:
∀L : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, L alpha p → PNo_downc L alpha p
L1252Axiom. (
PNo_upc_ref) We take the following as an axiom:
∀R : set → (set → prop) → prop, ∀alpha, ordinal alpha → ∀p : set → prop, R alpha p → PNo_upc R alpha p
L1254Axiom. (
PNoLe_upc) We take the following as an axiom:
L1258Definition. 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.
L1301Axiom. (
PNo_extend0_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta /\ delta <> alpha)
L1303Axiom. (
PNo_extend1_eq) We take the following as an axiom:
∀alpha, ∀p : set → prop, PNoEq_ alpha p (λdelta ⇒ p delta \/ delta = alpha)
L1311Definition. 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.
Primitive. The name
PNo_bd is a term of type
(set → (set → prop) → prop) → (set → (set → prop) → prop) → set.
Primitive. The name
PNo_pred is a term of type
(set → (set → prop) → prop) → (set → (set → prop) → prop) → set → prop.
L1420Axiom. (
PNo_bd_pred) We take the following as an axiom:
L1427Axiom. (
PNo_bd_In) We take the following as an axiom:
Beginning of Section TaggedSets
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
tag.
L1458Axiom. (
SNoElts_mon) We take the following as an axiom:
L1467Axiom. (
PNoEq_PSNo) We take the following as an axiom:
L1469Axiom. (
SNo_PSNo) We take the following as an axiom:
Primitive. The name
SNo is a term of type
set → prop.
L1476Axiom. (
SNo_SNo) We take the following as an axiom:
Primitive. The name
SNoLev is a term of type
set → set.
L1483Axiom. (
SNoLev_uniq) We take the following as an axiom:
L1485Axiom. (
SNoLev_prop) We take the following as an axiom:
L1489Axiom. (
SNoLev_) We take the following as an axiom:
L1493Axiom. (
SNoLev_PSNo) We take the following as an axiom:
L1495Axiom. (
SNo_Subq) We take the following as an axiom:
L1497Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) of type
set → set → set → prop.
L1500Axiom. (
SNoEq_I) We take the following as an axiom:
L1502Axiom. (
SNo_eq) We take the following as an axiom:
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.
L1516Axiom. (
SNoLtLe) We take the following as an axiom:
L1518Axiom. (
SNoLeE) We take the following as an axiom:
L1520Axiom. (
SNoEq_sym_) We take the following as an axiom:
L1522Axiom. (
SNoEq_tra_) We take the following as an axiom:
L1524Axiom. (
SNoLtE) We take the following as an axiom:
L1531Axiom. (
SNoLtI2) We take the following as an axiom:
L1539Axiom. (
SNoLtI3) We take the following as an axiom:
L1545Axiom. (
SNoLt_irref) We take the following as an axiom:
L1556Axiom. (
SNoLt_tra) We take the following as an axiom:
L1558Axiom. (
SNoLe_ref) We take the following as an axiom:
L1562Axiom. (
SNoLtLe_tra) We take the following as an axiom:
L1564Axiom. (
SNoLeLt_tra) We take the following as an axiom:
L1566Axiom. (
SNoLe_tra) We take the following as an axiom:
L1568Axiom. (
SNoLtLe_or) We take the following as an axiom:
L1581Definition. 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.
L1604Axiom. (
SNoCutP_L_0) We take the following as an axiom:
L1606Axiom. (
SNoCutP_0_R) We take the following as an axiom:
L1608Axiom. (
SNoCutP_0_0) We take the following as an axiom:
L1612Axiom. (
SNoS_E) We take the following as an axiom:
Beginning of Section TaggedSets2
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
tag.
L1619Axiom. (
SNoS_I) We take the following as an axiom:
L1621Axiom. (
SNoS_I2) We take the following as an axiom:
L1623Axiom. (
SNoS_Subq) We take the following as an axiom:
L1627Axiom. (
SNoS_E2) We take the following as an axiom:
L1632Axiom. (
SNoS_In_neq) We take the following as an axiom:
L1634Axiom. (
SNoS_SNoLev) We take the following as an axiom:
L1641Axiom. (
SNoL_E) We take the following as an axiom:
L1646Axiom. (
SNoR_E) We take the following as an axiom:
L1651Axiom. (
SNoL_SNoS_) We take the following as an axiom:
L1653Axiom. (
SNoR_SNoS_) We take the following as an axiom:
L1655Axiom. (
SNoL_SNoS) We take the following as an axiom:
L1657Axiom. (
SNoR_SNoS) We take the following as an axiom:
L1659Axiom. (
SNoL_I) We take the following as an axiom:
L1661Axiom. (
SNoR_I) We take the following as an axiom:
L1663Axiom. (
SNo_eta) We take the following as an axiom:
L1678Axiom. (
SNoCut_Le) We take the following as an axiom:
L1683Axiom. (
SNoCut_ext) We take the following as an axiom:
L1714Axiom. (
ordinal_SNo) We take the following as an axiom:
L1724Axiom. (
nat_p_SNo) We take the following as an axiom:
L1726Axiom. (
omega_SNo) We take the following as an axiom:
L1740Axiom. (
SNo_0) We take the following as an axiom:
L1742Axiom. (
SNo_1) We take the following as an axiom:
L1744Axiom. (
SNo_2) We take the following as an axiom:
L1746Axiom. (
SNoLev_0) We take the following as an axiom:
L1748Axiom. (
SNoCut_0_0) We take the following as an axiom:
L1750Axiom. (
SNoL_0) We take the following as an axiom:
L1752Axiom. (
SNoR_0) We take the following as an axiom:
L1754Axiom. (
SNoL_1) We take the following as an axiom:
L1756Axiom. (
SNoR_1) We take the following as an axiom:
L1790Axiom. (
SNo_0_eq_0) We take the following as an axiom:
L1797Axiom. (
eps_0_1) We take the following as an axiom:
L1799Axiom. (
SNo__eps_) We take the following as an axiom:
L1801Axiom. (
SNo_eps_) We take the following as an axiom:
L1803Axiom. (
SNo_eps_1) We take the following as an axiom:
L1805Axiom. (
SNoLev_eps_) We take the following as an axiom:
L1811Axiom. (
SNo_eps_pos) We take the following as an axiom:
L1817Axiom. (
eps_SNo_eq) We take the following as an axiom:
L1819Axiom. (
eps_SNoCutP) We take the following as an axiom:
L1821Axiom. (
eps_SNoCut) We take the following as an axiom:
End of Section TaggedSets2
L1825Axiom. (
SNo_etaE) We take the following as an axiom:
L1834Axiom. (
SNo_ind) We take the following as an axiom:
∀P : set → prop, (∀L R, SNoCutP L R → (∀x ∈ L, P x) → (∀y ∈ R, P y) → P (SNoCut L R)) → ∀z, SNo z → P z
Beginning of Section SurrealRecI
L1845Variable F : set → (set → set) → set
Primitive. The name
SNo_rec_i is a term of type
set → set.
L1861Hypothesis Fr : ∀z, SNo z → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
End of Section SurrealRecI
Beginning of Section SurrealRecII
L1871Variable F : set → (set → (set → set)) → (set → set)
L1874Let 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)
Primitive. The name
SNo_rec_ii is a term of type
set → (set → set).
L1885Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set), (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
End of Section SurrealRecII
Beginning of Section SurrealRec2
L1895Variable F : set → set → (set → set → set) → set
L1897Let 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)
Primitive. The name
SNo_rec2 is a term of type
set → set → set.
L1922Axiom. (
SNo_rec2_eq) We take the following as an axiom:
End of Section SurrealRec2
L1947Axiom. (
SNoLev_ind) We take the following as an axiom:
L1952Axiom. (
SNoLev_ind2) We take the following as an axiom:
L1960Axiom. (
SNoLev_ind3) We take the following as an axiom:
∀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
L1972Axiom. (
SNo_omega) We take the following as an axiom:
L1974Axiom. (
SNoLt_0_1) We take the following as an axiom:
L1976Axiom. (
SNoLt_0_2) We take the following as an axiom:
L1978Axiom. (
SNoLt_1_2) We take the following as an axiom:
L1980Axiom. (
restr_SNo_) We take the following as an axiom:
L1982Axiom. (
restr_SNo) We take the following as an axiom:
L1986Axiom. (
restr_SNoEq) We take the following as an axiom:
Beginning of Section SurrealMinus
Primitive. The name
minus_SNo is a term of type
set → set.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Notation. We use
<= as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe.
End of Section SurrealMinus
Beginning of Section SurrealAdd
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_SNo.
Primitive. The name
add_SNo is a term of type
set → set → set.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_SNo.
L2055Axiom. (
add_SNo_eq) We take the following as an axiom:
L2066Axiom. (
SNo_add_SNo) We take the following as an axiom:
L2074Axiom. (
add_SNo_Lt1) We take the following as an axiom:
L2076Axiom. (
add_SNo_Le1) We take the following as an axiom:
L2078Axiom. (
add_SNo_Lt2) We take the following as an axiom:
L2080Axiom. (
add_SNo_Le2) We take the following as an axiom:
L2086Axiom. (
add_SNo_Lt3) We take the following as an axiom:
L2088Axiom. (
add_SNo_Le3) We take the following as an axiom:
L2092Axiom. (
add_SNo_com) We take the following as an axiom:
L2094Axiom. (
add_SNo_0L) We take the following as an axiom:
L2096Axiom. (
add_SNo_0R) We take the following as an axiom:
L2130Axiom. (
minus_SNo_0) We take the following as an axiom:
L2246Axiom. (
add_SNo_Lt4) We take the following as an axiom:
End of Section SurrealAdd
Notation. We use
:*: as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod.
Notation. We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp.
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.
Primitive. The name
mul_SNo is a term 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_SNo.
L2323Axiom. (
mul_SNo_eq) We take the following as an axiom:
L2332Axiom. (
mul_SNo_eq_2) We take the following as an axiom:
∀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
L2353Axiom. (
mul_SNo_prop_1) We take the following as an axiom:
∀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
L2363Axiom. (
SNo_mul_SNo) We take the following as an axiom:
L2369Axiom. (
mul_SNo_eq_3) We take the following as an axiom:
∀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
L2390Axiom. (
mul_SNo_Lt) We take the following as an axiom:
L2393Axiom. (
mul_SNo_Le) We take the following as an axiom:
L2418Axiom. (
mul_SNo_Subq_lem) We take the following as an axiom:
∀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'
L2436Axiom. (
mul_SNo_com) We take the following as an axiom:
Beginning of Section mul_SNo_assoc_lems
L2450Variable 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.
L2453Hypothesis SNo_M : ∀x y, SNo x → SNo y → SNo (x * y)
L2455Hypothesis DL : ∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z
L2457Hypothesis DR : ∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z
L2468Hypothesis 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
L2473Axiom. (
mul_SNo_assoc_lem1) We take the following as an axiom:
∀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
L2489Axiom. (
mul_SNo_assoc_lem2) We take the following as an axiom:
∀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
End of Section mul_SNo_assoc_lems
L2562Axiom. (
SNo_foil) We take the following as an axiom:
L2581Axiom. (
SNo_foil_mm) We take the following as an axiom:
L2585Axiom. (
mul_SNoCutP_lem) We take the following as an axiom:
∀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
L2642Axiom. (
mul_SNoCut_abs) We take the following as an axiom:
∀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
End of Section SurrealMul
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.
L2738Axiom. (
eps_bd_1) We take the following as an axiom:
L2752Axiom. (
SNoS_finite) We take the following as an axiom:
End of Section SurrealExp
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.
L2774Axiom. (
int_3_cases) We take the following as an axiom:
L2780Axiom. (
int_SNo) We take the following as an axiom:
L2788Axiom. (
int_add_SNo) We take the following as an axiom:
L2792Axiom. (
int_mul_SNo) We take the following as an axiom:
End of Section Int
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.
L2808Axiom. (
abs_SNo_0) We take the following as an axiom:
L2810Axiom. (
pos_abs_SNo) We take the following as an axiom:
L2812Axiom. (
neg_abs_SNo) We take the following as an axiom:
L2814Axiom. (
SNo_abs_SNo) We take the following as an axiom:
L2816Axiom. (
abs_SNo_Lev) We take the following as an axiom:
End of Section SurrealAbs
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.
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.
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.
L2919Definition. 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.
Beginning of Section recip_SNo_pos
End of Section recip_SNo_pos
L2993Axiom. (
recip_SNo_0) We take the following as an axiom:
L2995Axiom. (
recip_SNo_1) We take the following as an axiom:
L3007Axiom. (
recip_SNo_2) We take the following as an axiom:
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_SNo.
L3019Axiom. (
SNo_div_SNo) We take the following as an axiom:
L3035Axiom. (
div_div_SNo) We take the following as an axiom:
End of Section SurrealDiv
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.
Beginning of Section sqrt_SNo_nonneg
End of Section sqrt_SNo_nonneg
End of Section SurrealSqrt
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 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.
L3223Axiom. (
real_I) We take the following as an axiom:
L3229Axiom. (
real_E) We take the following as an axiom:
L3241Axiom. (
real_SNo) We take the following as an axiom:
L3247Axiom. (
real_0) We take the following as an axiom:
L3249Axiom. (
real_1) We take the following as an axiom:
L3260Axiom. (
real_SNoCut) We take the following as an axiom:
L3330Axiom. (
SNo_approx_real_rep) We take the following as an axiom:
∀x ∈ real, ∀p : prop, (∀f g ∈ SNoS_ omega :^: omega, (∀n ∈ omega, f n < x) → (∀n ∈ omega, x < f n + eps_ n) → (∀n ∈ omega, ∀i ∈ n, f i < f n) → (∀n ∈ omega, g n + - eps_ n < x) → (∀n ∈ omega, x < g n) → (∀n ∈ omega, ∀i ∈ n, g n < g i) → SNoCutP {f n|n ∈ omega} {g n|n ∈ omega} → x = SNoCut {f n|n ∈ omega} {g n|n ∈ omega} → p) → p
End of Section Reals
L3400Axiom. (
mul_nat_1R) We take the following as an axiom:
L3407Axiom. (
mul_nat_com) We take the following as an axiom:
L3409Axiom. (
mul_nat_SL) We take the following as an axiom:
L3432Axiom. (
even_nat_0) We take the following as an axiom:
L3438Axiom. (
odd_nat_1) We take the following as an axiom:
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.
Beginning of Section Alg
L3489Variable extension_tag : set
L3491Let ctag : set → set ≝ λalpha ⇒ SetAdjoin alpha extension_tag
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag.
L3494Variable F : set → prop
L3496Hypothesis extension_tag_fresh : ∀x, F x → ∀u ∈ x, extension_tag /:e u
L3502Axiom. (
ctagged_eqE_eq) We take the following as an axiom:
∀x y, F x → F y → ∀u ∈ x, ∀v ∈ y, u '' = v '' → u = v
L3512Axiom. (
pair_tag_0) We take the following as an axiom:
L3514Definition. We define
CD_carr to be
λz ⇒ exists x, F x /\ exists y, F y /\ z = pair_tag x y of type
set → prop.
L3516Axiom. (
CD_carr_I) We take the following as an axiom:
L3518Axiom. (
CD_carr_E) We take the following as an axiom:
L3532Axiom. (
CD_proj0_1) We take the following as an axiom:
∀z, CD_carr z → F (proj0 z) /\ exists y, F y /\ z = pa (proj0 z) y
L3534Axiom. (
CD_proj0_2) We take the following as an axiom:
∀x y, F x → F y → proj0 (pa x y) = x
L3536Axiom. (
CD_proj1_1) We take the following as an axiom:
∀z, CD_carr z → F (proj1 z) /\ z = pa (proj0 z) (proj1 z)
L3538Axiom. (
CD_proj1_2) We take the following as an axiom:
∀x y, F x → F y → proj1 (pa x y) = y
L3540Axiom. (
CD_proj0R) We take the following as an axiom:
L3542Axiom. (
CD_proj1R) We take the following as an axiom:
L3548Axiom. (
CD_proj0_F) We take the following as an axiom:
L3550Axiom. (
CD_proj1_F) We take the following as an axiom:
Beginning of Section CD_minus_conj
L3554Variable minus : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
L3557Definition. We define
CD_minus to be
λz ⇒ pa (- proj0 z) (- proj1 z) of type
set → set.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus.
L3561Variable conj : set → set
L3564Definition. We define
CD_conj to be
λz ⇒ pa (conj (proj0 z)) (- proj1 z) of type
set → set.
End of Section CD_minus_conj
Beginning of Section CD_add
L3569Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
L3572Definition. We define
CD_add to be
λz w ⇒ pa (proj0 z + proj0 w) (proj1 z + proj1 w) of type
set → set → set.
End of Section CD_add
Beginning of Section CD_mul
L3578Variable minus : set → set
L3580Variable conj : set → set
L3581Variable add : set → set → set
L3582Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
L3587Definition. We define
CD_mul to be
λz w ⇒ pa (proj0 z * proj0 w + - conj (proj1 w) * proj1 z) (proj1 w * proj0 z + proj1 z * conj (proj0 w)) 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
CD_mul.
End of Section CD_mul
Beginning of Section CD_minus_conj_clos
L3596Variable minus : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
L3600Hypothesis F_minus : ∀x, F x → F (- x)
L3602Axiom. (
CD_minus_CD) We take the following as an axiom:
L3608Variable conj : set → set
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
L3611Hypothesis F_conj : ∀x, F x → F (conj x)
L3613Axiom. (
CD_conj_CD) We take the following as an axiom:
End of Section CD_minus_conj_clos
Beginning of Section CD_add_clos
L3623Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3627Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L3629Axiom. (
CD_add_CD) We take the following as an axiom:
End of Section CD_add_clos
Beginning of Section CD_mul_clos
L3639Variable minus : set → set
L3641Variable conj : set → set
L3642Variable add : set → set → set
L3643Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L3653Hypothesis F_minus : ∀x, F x → F (- x)
L3655Hypothesis F_conj : ∀x, F x → F (conj x)
L3656Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L3657Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L3658Axiom. (
CD_mul_CD) We take the following as an axiom:
End of Section CD_mul_clos
Beginning of Section CD_minus_conj_F
L3668Variable minus : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
L3674Hypothesis F_minus_0 : - 0 = 0
L3677Variable conj : set → set
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
End of Section CD_minus_conj_F
Beginning of Section CD_add_F
L3686Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3693Hypothesis F_add_0_0 : 0 + 0 = 0
L3694Axiom. (
CD_add_F_eq) We take the following as an axiom:
∀x y, F x → F y → x :+: y = x + y
End of Section CD_add_F
Beginning of Section CD_mul_F
L3700Variable minus : set → set
L3702Variable conj : set → set
L3703Variable add : set → set → set
L3704Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L3716Hypothesis F_conj : ∀x, F x → F (conj x)
L3717Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L3718Hypothesis F_minus_0 : - 0 = 0
L3719Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L3720Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L3721Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L3722Axiom. (
CD_mul_F_eq) We take the following as an axiom:
∀x y, F x → F y → x :*: y = x * y
End of Section CD_mul_F
Beginning of Section CD_minus_invol
L3728Variable minus : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
L3732Hypothesis F_minus : ∀x, F x → F (- x)
L3734Hypothesis F_minus_invol : ∀x, F x → - - x = x
End of Section CD_minus_invol
Beginning of Section CD_conj_invol
L3741Variable minus : set → set
L3743Variable conj : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
L3748Hypothesis F_minus : ∀x, F x → F (- x)
L3750Hypothesis F_conj : ∀x, F x → F (conj x)
L3751Hypothesis F_minus_invol : ∀x, F x → - - x = x
L3752Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x
End of Section CD_conj_invol
Beginning of Section CD_conj_minus
L3759Variable minus : set → set
L3761Variable conj : set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
L3766Hypothesis F_minus : ∀x, F x → F (- x)
L3768Hypothesis F_conj : ∀x, F x → F (conj x)
L3769Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
End of Section CD_conj_minus
Beginning of Section CD_minus_add
L3776Variable minus : set → set
L3778Variable add : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3785Hypothesis F_minus : ∀x, F x → F (- x)
L3787Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L3788Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
End of Section CD_minus_add
Beginning of Section CD_conj_add
L3795Variable minus : set → set
L3797Variable conj : set → set
L3798Variable add : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3806Hypothesis F_minus : ∀x, F x → F (- x)
L3808Hypothesis F_conj : ∀x, F x → F (conj x)
L3809Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L3810Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L3811Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
L3812Axiom. (
CD_conj_add) We take the following as an axiom:
End of Section CD_conj_add
Beginning of Section CD_add_com
L3818Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3822Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L3824Axiom. (
CD_add_com) We take the following as an axiom:
End of Section CD_add_com
Beginning of Section CD_add_assoc
L3830Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3834Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L3836Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
End of Section CD_add_assoc
Beginning of Section CD_add_0R
L3843Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3849Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L3850Axiom. (
CD_add_0R) We take the following as an axiom:
End of Section CD_add_0R
Beginning of Section CD_add_0L
L3856Variable add : set → set → set
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3862Hypothesis F_add_0L : ∀x, F x → 0 + x = x
L3863Axiom. (
CD_add_0L) We take the following as an axiom:
End of Section CD_add_0L
Beginning of Section CD_add_minus_linv
L3869Variable minus : set → set
L3871Variable add : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3876Hypothesis F_minus : ∀x, F x → F (- x)
L3878Hypothesis F_add_minus_linv : ∀x, F x → - x + x = 0
End of Section CD_add_minus_linv
Beginning of Section CD_add_minus_rinv
L3885Variable minus : set → set
L3887Variable add : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
L3892Hypothesis F_minus : ∀x, F x → F (- x)
L3894Hypothesis F_add_minus_rinv : ∀x, F x → x + - x = 0
End of Section CD_add_minus_rinv
Beginning of Section CD_mul_0R
L3901Variable minus : set → set
L3903Variable conj : set → set
L3904Variable add : set → set → set
L3905Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L3916Hypothesis F_minus_0 : - 0 = 0
L3917Hypothesis F_conj_0 : conj 0 = 0
L3918Hypothesis F_add_0_0 : 0 + 0 = 0
L3919Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L3920Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L3921Axiom. (
CD_mul_0R) We take the following as an axiom:
End of Section CD_mul_0R
Beginning of Section CD_mul_0L
L3927Variable minus : set → set
L3929Variable conj : set → set
L3930Variable add : set → set → set
L3931Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L3942Hypothesis F_conj : ∀x, F x → F (conj x)
L3943Hypothesis F_minus_0 : - 0 = 0
L3944Hypothesis F_add_0_0 : 0 + 0 = 0
L3945Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L3946Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L3947Axiom. (
CD_mul_0L) We take the following as an axiom:
End of Section CD_mul_0L
Beginning of Section CD_mul_1R
L3953Variable minus : set → set
L3955Variable conj : set → set
L3956Variable add : set → set → set
L3957Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L3969Hypothesis F_minus_0 : - 0 = 0
L3970Hypothesis F_conj_0 : conj 0 = 0
L3971Hypothesis F_conj_1 : conj 1 = 1
L3972Hypothesis F_add_0L : ∀x, F x → 0 + x = x
L3973Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L3974Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L3975Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
L3976Axiom. (
CD_mul_1R) We take the following as an axiom:
End of Section CD_mul_1R
Beginning of Section CD_mul_1L
L3982Variable minus : set → set
L3984Variable conj : set → set
L3985Variable add : set → set → set
L3986Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L3998Hypothesis F_conj : ∀x, F x → F (conj x)
L3999Hypothesis F_minus_0 : - 0 = 0
L4000Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L4001Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L4002Hypothesis F_mul_0R : ∀x, F x → x * 0 = 0
L4003Hypothesis F_mul_1L : ∀x, F x → 1 * x = x
L4004Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
L4005Axiom. (
CD_mul_1L) We take the following as an axiom:
End of Section CD_mul_1L
Beginning of Section CD_conj_mul
L4011Variable minus : set → set
L4013Variable conj : set → set
L4014Variable add : set → set → set
L4015Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L4024Hypothesis F_minus : ∀x, F x → F (- x)
L4026Hypothesis F_conj : ∀x, F x → F (conj x)
L4027Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L4028Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L4029Hypothesis F_minus_invol : ∀x, F x → - - x = x
L4030Hypothesis F_conj_invol : ∀x, F x → conj (conj x) = x
L4031Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
L4032Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
L4033Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L4034Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L4035Hypothesis F_conj_mul : ∀x y, F x → F y → conj (x * y) = conj y * conj x
L4036Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
L4037Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
L4038Axiom. (
CD_conj_mul) We take the following as an axiom:
End of Section CD_conj_mul
Beginning of Section CD_add_mul_distrR
L4044Variable minus : set → set
L4046Variable conj : set → set
L4047Variable add : set → set → set
L4048Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L4057Hypothesis F_minus : ∀x, F x → F (- x)
L4059Hypothesis F_conj : ∀x, F x → F (conj x)
L4060Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L4061Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L4062Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L4063Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
L4064Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L4065Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z
L4066Hypothesis F_add_mul_distrR : ∀x y z, F x → F y → F z → (x + y) * z = x * z + y * z
End of Section CD_add_mul_distrR
Beginning of Section CD_add_mul_distrL
L4073Variable minus : set → set
L4075Variable conj : set → set
L4076Variable add : set → set → set
L4077Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L4086Hypothesis F_minus : ∀x, F x → F (- x)
L4088Hypothesis F_conj : ∀x, F x → F (conj x)
L4089Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L4090Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L4091Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L4092Hypothesis F_conj_add : ∀x y, F x → F y → conj (x + y) = conj x + conj y
L4093Hypothesis F_add_assoc : ∀x y z, F x → F y → F z → (x + y) + z = x + (y + z)
L4094Hypothesis F_add_com : ∀x y, F x → F y → x + y = y + x
L4095Hypothesis F_add_mul_distrL : ∀x y z, F x → F y → F z → x * (y + z) = x * y + x * z
L4096Hypothesis F_add_mul_distrR : ∀x y z, F x → F y → F z → (x + y) * z = x * z + y * z
End of Section CD_add_mul_distrL
Beginning of Section CD_minus_mul_distrR
L4103Variable minus : set → set
L4105Variable conj : set → set
L4106Variable add : set → set → set
L4107Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L4116Hypothesis F_minus : ∀x, F x → F (- x)
L4118Hypothesis F_conj : ∀x, F x → F (conj x)
L4119Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L4120Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L4121Hypothesis F_conj_minus : ∀x, F x → conj (- x) = - conj x
L4122Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L4123Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
L4124Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
End of Section CD_minus_mul_distrR
Beginning of Section CD_minus_mul_distrL
L4131Variable minus : set → set
L4133Variable conj : set → set
L4134Variable add : set → set → set
L4135Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
L4144Hypothesis F_minus : ∀x, F x → F (- x)
L4146Hypothesis F_conj : ∀x, F x → F (conj x)
L4147Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L4148Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
L4149Hypothesis F_minus_add : ∀x y, F x → F y → - (x + y) = - x + - y
L4150Hypothesis F_minus_mul_distrR : ∀x y, F x → F y → x * (- y) = - (x * y)
L4151Hypothesis F_minus_mul_distrL : ∀x y, F x → F y → (- x) * y = - (x * y)
End of Section CD_minus_mul_distrL
Beginning of Section CD_exp_nat
L4158Variable minus : set → set
L4160Variable conj : set → set
L4161Variable add : set → set → set
L4162Variable mul : set → set → set
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
conj.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul.
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
CD_minus minus.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
CD_conj minus conj.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
CD_add add.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
CD_mul minus conj add mul.
Notation. We use
^ as an infix operator with priority 342 and no associativity corresponding to applying term
CD_exp_nat minus conj add mul.
Beginning of Section CD_exp_nat_1_2
L4183Hypothesis F_minus_0 : - 0 = 0
L4184Hypothesis F_conj_0 : conj 0 = 0
L4185Hypothesis F_conj_1 : conj 1 = 1
L4186Hypothesis F_add_0L : ∀x, F x → 0 + x = x
L4187Hypothesis F_add_0R : ∀x, F x → x + 0 = x
L4188Hypothesis F_mul_0L : ∀x, F x → 0 * x = 0
L4189Hypothesis F_mul_1R : ∀x, F x → x * 1 = x
End of Section CD_exp_nat_1_2
L4196Hypothesis F_minus : ∀x, F x → F (- x)
L4198Hypothesis F_conj : ∀x, F x → F (conj x)
L4199Hypothesis F_add : ∀x y, F x → F y → F (x + y)
L4200Hypothesis F_mul : ∀x y, F x → F y → F (x * y)
End of Section CD_exp_nat
End of Section Alg
Beginning of Section Tags
L4216Hypothesis tagn_nat : nat_p tagn
L4217Hypothesis tagn_1 : 1 ∈ tagn
End of Section Tags
Beginning of Section ExtendedSNo
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
tag.
End of Section ExtendedSNo
Beginning of Section SurComplex
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
tag.
L4248Axiom. (
SNo_pair_0) We take the following as an axiom:
L4256Axiom. (
CSNo_I) We take the following as an axiom:
L4258Axiom. (
CSNo_E) We take the following as an axiom:
L4263Axiom. (
SNo_CSNo) We take the following as an axiom:
L4265Axiom. (
CSNo_0) We take the following as an axiom:
L4267Axiom. (
CSNo_1) We take the following as an axiom:
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag.
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.
L4289Axiom. (
CSNo_Re1) We take the following as an axiom:
L4291Axiom. (
CSNo_Re2) We take the following as an axiom:
∀x y, SNo x → SNo y → Re (pa x y) = x
L4293Axiom. (
CSNo_Im1) We take the following as an axiom:
L4295Axiom. (
CSNo_Im2) We take the following as an axiom:
∀x y, SNo x → SNo y → Im (pa x y) = y
L4297Axiom. (
CSNo_ReR) We take the following as an axiom:
L4299Axiom. (
CSNo_ImR) We take the following as an axiom:
L4301Axiom. (
CSNo_ReIm) We take the following as an axiom:
∀z, CSNo z → z = pa (Re z) (Im z)
L4309Let conj : set → set ≝ λx ⇒ x
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
minus_CSNo.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
conj_CSNo.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_CSNo.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_CSNo.
Notation. We use
:^: as an infix operator with priority 355 and which associates to the right corresponding to applying term
exp_CSNo_nat.
L4358Axiom. (
mul_CSNo_CRe) We take the following as an axiom:
∀z w, CSNo z → CSNo w → Re (mult' z w) = Re z * Re w + - (Im w * Im z)
L4360Axiom. (
mul_CSNo_CIm) We take the following as an axiom:
∀z w, CSNo z → CSNo w → Im (mult' z w) = Im w * Re z + Im z * Re w
L4362Axiom. (
SNo_Re) We take the following as an axiom:
L4364Axiom. (
SNo_Im) We take the following as an axiom:
L4366Axiom. (
Re_0) We take the following as an axiom:
L4368Axiom. (
Im_0) We take the following as an axiom:
L4370Axiom. (
Re_1) We take the following as an axiom:
L4372Axiom. (
Im_1) We take the following as an axiom:
L4374Axiom. (
Re_i) We take the following as an axiom:
L4376Axiom. (
Im_i) We take the following as an axiom:
L4380Axiom. (
conj_CSNo_0) We take the following as an axiom:
L4382Axiom. (
conj_CSNo_1) We take the following as an axiom:
L4384Axiom. (
conj_CSNo_i) We take the following as an axiom:
L4408Axiom. (
add_CSNo_0L) We take the following as an axiom:
L4410Axiom. (
add_CSNo_0R) We take the following as an axiom:
L4416Axiom. (
mul_CSNo_0R) We take the following as an axiom:
L4418Axiom. (
mul_CSNo_0L) We take the following as an axiom:
L4420Axiom. (
mul_CSNo_1R) We take the following as an axiom:
L4422Axiom. (
mul_CSNo_1L) We take the following as an axiom:
End of Section SurComplex
Beginning of Section Complex
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_CSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_CSNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_CSNo.
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.
L4514Axiom. (
complex_I) We take the following as an axiom:
L4516Axiom. (
complex_E) We take the following as an axiom:
L4524Axiom. (
complex_0) We take the following as an axiom:
L4526Axiom. (
complex_1) We take the following as an axiom:
L4528Axiom. (
complex_i) We take the following as an axiom:
L4548Axiom. (
real_Re_eq) We take the following as an axiom:
L4550Axiom. (
real_Im_eq) We take the following as an axiom:
L4558Axiom. (
complex_eta) We take the following as an axiom:
Beginning of Section ComplexDiv
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.
End of Section ComplexDiv
End of Section Complex
Beginning of Section SurQuaternions
L4585Axiom. (
CSNo_pair_0) We take the following as an axiom:
L4593Axiom. (
HSNo_I) We take the following as an axiom:
L4595Axiom. (
HSNo_E) We take the following as an axiom:
L4600Axiom. (
CSNo_HSNo) We take the following as an axiom:
L4602Axiom. (
HSNo_0) We take the following as an axiom:
L4604Axiom. (
HSNo_1) We take the following as an axiom:
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_CSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_CSNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_CSNo.
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_CSNo.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
conj_CSNo.
L4639Axiom. (
HSNo_proj0R) We take the following as an axiom:
L4641Axiom. (
HSNo_proj1R) We take the following as an axiom:
L4643Axiom. (
HSNo_proj0p1) We take the following as an axiom:
∀z, HSNo z → z = pa (p0 z) (p1 z)
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
minus_HSNo.
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
conj_HSNo.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_HSNo.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_HSNo.
Notation. We use
:^: as an infix operator with priority 355 and which associates to the right corresponding to applying term
exp_HSNo_nat.
L4700Axiom. (
HSNo_p0_0) We take the following as an axiom:
L4702Axiom. (
HSNo_p1_0) We take the following as an axiom:
L4704Axiom. (
HSNo_p0_1) We take the following as an axiom:
L4706Axiom. (
HSNo_p1_1) We take the following as an axiom:
L4708Axiom. (
HSNo_p0_i) We take the following as an axiom:
L4710Axiom. (
HSNo_p1_i) We take the following as an axiom:
L4712Axiom. (
HSNo_p0_j) We take the following as an axiom:
L4714Axiom. (
HSNo_p1_j) We take the following as an axiom:
L4716Axiom. (
HSNo_p0_k) We take the following as an axiom:
L4718Axiom. (
HSNo_p1_k) We take the following as an axiom:
L4728Axiom. (
conj_HSNo_0) We take the following as an axiom:
L4730Axiom. (
conj_HSNo_1) We take the following as an axiom:
L4750Axiom. (
add_HSNo_0L) We take the following as an axiom:
L4752Axiom. (
add_HSNo_0R) We take the following as an axiom:
L4758Axiom. (
mul_HSNo_0R) We take the following as an axiom:
L4760Axiom. (
mul_HSNo_0L) We take the following as an axiom:
L4762Axiom. (
mul_HSNo_1R) We take the following as an axiom:
L4764Axiom. (
mul_HSNo_1L) We take the following as an axiom:
L4820Axiom. (
conj_HSNo_i) We take the following as an axiom:
L4822Axiom. (
conj_HSNo_j) We take the following as an axiom:
L4824Axiom. (
conj_HSNo_k) We take the following as an axiom:
End of Section SurQuaternions
Beginning of Section Quaternions
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_HSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_HSNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_HSNo.
End of Section Quaternions
Beginning of Section SurOctonions
L4894Axiom. (
HSNo_pair_0) We take the following as an axiom:
L4902Axiom. (
OSNo_I) We take the following as an axiom:
L4904Axiom. (
OSNo_E) We take the following as an axiom:
L4909Axiom. (
HSNo_OSNo) We take the following as an axiom:
L4911Axiom. (
OSNo_0) We take the following as an axiom:
L4913Axiom. (
OSNo_1) We take the following as an axiom:
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
ctag.
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_HSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_HSNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_HSNo.
Notation. We use
:/: as an infix operator with priority 353 and no associativity corresponding to applying term
div_HSNo.
Notation. We use
' as a postfix operator with priority 100 corresponding to applying term
conj_HSNo.
L4945Axiom. (
OSNo_proj0R) We take the following as an axiom:
L4947Axiom. (
OSNo_proj1R) We take the following as an axiom:
L4949Axiom. (
OSNo_proj0p1) We take the following as an axiom:
∀z, OSNo z → z = pa (p0 z) (p1 z)
Notation. We use
:-: as a prefix operator with priority 358 corresponding to applying term
minus_OSNo.
Notation. We use
'' as a postfix operator with priority 100 corresponding to applying term
conj_OSNo.
Notation. We use
:+: as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_OSNo.
Notation. We use
:*: as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_OSNo.
Notation. We use
:^: as an infix operator with priority 355 and which associates to the right corresponding to applying term
exp_OSNo_nat.
L5000Axiom. (
OSNo_p0_0) We take the following as an axiom:
L5002Axiom. (
OSNo_p1_0) We take the following as an axiom:
L5004Axiom. (
OSNo_p0_1) We take the following as an axiom:
L5006Axiom. (
OSNo_p1_1) We take the following as an axiom:
L5008Axiom. (
OSNo_p0_i) We take the following as an axiom:
L5010Axiom. (
OSNo_p1_i) We take the following as an axiom:
L5012Axiom. (
OSNo_p0_j) We take the following as an axiom:
L5014Axiom. (
OSNo_p1_j) We take the following as an axiom:
L5016Axiom. (
OSNo_p0_k) We take the following as an axiom:
L5018Axiom. (
OSNo_p1_k) We take the following as an axiom:
L5026Axiom. (
conj_OSNo_0) We take the following as an axiom:
L5028Axiom. (
conj_OSNo_1) We take the following as an axiom:
L5048Axiom. (
add_OSNo_0L) We take the following as an axiom:
L5050Axiom. (
add_OSNo_0R) We take the following as an axiom:
L5056Axiom. (
mul_OSNo_0R) We take the following as an axiom:
L5058Axiom. (
mul_OSNo_0L) We take the following as an axiom:
L5060Axiom. (
mul_OSNo_1R) We take the following as an axiom:
L5062Axiom. (
mul_OSNo_1L) We take the following as an axiom:
L5119Axiom. (
OSNo_p0_i0) We take the following as an axiom:
L5121Axiom. (
OSNo_p1_i0) We take the following as an axiom:
L5123Axiom. (
OSNo_p0_i3) We take the following as an axiom:
L5125Axiom. (
OSNo_p1_i3) We take the following as an axiom:
L5127Axiom. (
OSNo_p0_i5) We take the following as an axiom:
L5129Axiom. (
OSNo_p1_i5) We take the following as an axiom:
L5131Axiom. (
OSNo_p0_i6) We take the following as an axiom:
L5133Axiom. (
OSNo_p1_i6) We take the following as an axiom:
End of Section SurOctonions
Beginning of Section Octonions
Notation. We use
- as a prefix operator with priority 358 corresponding to applying term
minus_OSNo.
Notation. We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_OSNo.
Notation. We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_OSNo.
L5257Axiom. (
octonion_I) We take the following as an axiom:
L5259Axiom. (
octonion_E) We take the following as an axiom:
L5267Axiom. (
octonion_0) We take the following as an axiom:
L5269Axiom. (
octonion_1) We take the following as an axiom:
L5271Axiom. (
octonion_i) We take the following as an axiom:
L5273Axiom. (
octonion_j) We take the following as an axiom:
L5275Axiom. (
octonion_k) We take the following as an axiom:
L5277Axiom. (
octonion_i0) We take the following as an axiom:
L5279Axiom. (
octonion_i3) We take the following as an axiom:
L5281Axiom. (
octonion_i5) We take the following as an axiom:
L5283Axiom. (
octonion_i6) We take the following as an axiom:
End of Section Octonions