Beginning of Section Eq
Variable A : SType
End of Section Eq
Beginning of Section FE
Variable A B : SType
Axiom. (func_ext) We take the following as an axiom:
∀f g : A → B, (∀x : A, f x = g x) → f = g
End of Section FE
Beginning of Section Ex
Variable A : SType
End of Section Ex
Axiom. (In_ind) We take the following as an axiom:
∀P : set → prop, (∀X : set, (∀x ∈ X, P x) → P X) → ∀X : set, P X
Axiom. (ReplEq) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} ↔ ∃x ∈ A, y = F x
Axiom. (andI) We take the following as an axiom:
∀A B : prop, A → B → A ∧ B
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (and3I) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
Axiom. (and3E) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop, (P1 → P2 → P3 → p) → p)
Axiom. (or3E) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop, (P1 → p) → (P2 → p) → (P3 → p) → p)
Variable P4 : prop
Axiom. (and4I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
Variable P5 : prop
Axiom. (and5I) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
End of Section PropN
Axiom. (iffI) We take the following as an axiom:
∀A B : prop, (A → B) → (B → A) → (A ↔ B)
Axiom. (iffEL) We take the following as an axiom:
∀A B : prop, (A ↔ B) → A → B
Axiom. (iffER) We take the following as an axiom:
∀A B : prop, (A ↔ B) → B → A
Axiom. (f_eq_i) We take the following as an axiom:
∀f : set → set, ∀x y, x = y → f x = f y
Axiom. (pred_ext) We take the following as an axiom:
∀P Q : set → prop, (∀x, P x ↔ Q x) → P = Q
Axiom. (ReplI) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}
Axiom. (ReplE) We take the following as an axiom:
∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∃x ∈ A, y = F x
Axiom. (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
Axiom. (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
Axiom. (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
Axiom. (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
Axiom. (binunionE') We take the following as an axiom:
∀X Y z, ∀p : prop, (z ∈ X → p) → (z ∈ Y → p) → (z ∈ X ∪ Y → p)
Axiom. (famunionI) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀x y : set, x ∈ X → y ∈ F x → y ∈ ⋃x ∈ XF x
Axiom. (famunionE) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∃x ∈ X, y ∈ F x
Axiom. (famunionE_impred) We take the following as an axiom:
∀X : set, ∀F : (set → set), ∀y : set, y ∈ (⋃x ∈ XF x) → ∀p : prop, (∀x, x ∈ X → y ∈ F x → p) → p
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z)
End of Section SepSec
Axiom. (SepI) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}
Axiom. (SepE) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X ∧ P x
Axiom. (SepE1) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
Axiom. (SepE2) We take the following as an axiom:
∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
Axiom. (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}
Axiom. (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} → ∃x : set, x ∈ X ∧ P x ∧ y = F x
Axiom. (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
Axiom. (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, ∃u ∈ X, f u = w) → bij X Y f
Axiom. (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, ∃u ∈ X, f u = w) → p) → p
Axiom. (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
Axiom. (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))
Beginning of Section SchroederBernstein
End of Section SchroederBernstein
Beginning of Section PigeonHole
End of Section PigeonHole
Axiom. (exandE_i) We take the following as an axiom:
∀P Q : set → prop, (∃x, P x ∧ Q x) → ∀r : prop, (∀x, P x → Q x → r) → r
Axiom. (exandE_ii) We take the following as an axiom:
∀P Q : (set → set) → prop, (∃x : set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set, P x → Q x → p) → p
Axiom. (exandE_iii) We take the following as an axiom:
∀P Q : (set → set → set) → prop, (∃x : set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set, P x → Q x → p) → p
Axiom. (exandE_iiii) We take the following as an axiom:
∀P Q : (set → set → set → set) → prop, (∃x : set → set → set → set, P x ∧ Q x) → ∀p : prop, (∀x : set → set → set → set, P x → Q x → p) → p
Beginning of Section Descr_ii
Variable P : (set → set) → prop
Hypothesis Pex : ∃f : set → set, P f
Hypothesis Puniq : ∀f g : set → set, P f → P g → f = g
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set) → prop
Hypothesis Pex : ∃f : set → set → set, P f
Hypothesis Puniq : ∀f g : set → set → set, P f → P g → f = g
End of Section Descr_iii
Beginning of Section Descr_Vo1
Hypothesis Pex : ∃f : Vo 1, P f
Hypothesis Puniq : ∀f g : Vo 1, P f → P g → f = g
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set) → set
Hypothesis Fr : ∀X : set, ∀g h : set → set, (∀x ∈ X, g x = h x) → F X g = F X h
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set)) → (set → set)
Hypothesis 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
Variable F : set → (set → (set → set → set)) → (set → set → set)
Hypothesis 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
Variable z : set
Variable f : set → set → set
Let F : set → (set → set) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n) (g (⋃ n)) else z
Axiom. (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
End of Section NatArith
Beginning of Section pair_setsum
Axiom. (pairI0) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
Axiom. (pairI1) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
Axiom. (pairE) We take the following as an axiom:
∀X Y z, z ∈ pair X Y → (∃x ∈ X, z = pair 0 x) ∨ (∃y ∈ Y, z = pair 1 y)
Axiom. (pairE0) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
Axiom. (pairE1) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
Axiom. (pair_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x ∈ X, ∀y ∈ Y x, pair x y ∈ ∑x ∈ X, Y x
Axiom. (pair_Sigma_E1) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀x y : set, pair x y ∈ (∑x ∈ X, Y x) → y ∈ Y x
Axiom. (Sigma_E) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → ∃x ∈ X, ∃y ∈ Y x, z = pair x y
Let lam : set → (set → set) → set ≝ Sigma
Axiom. (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
Axiom. (lamE) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀z : set, z ∈ (λx ∈ X ⇒ F x) → ∃x ∈ X, ∃y ∈ F x, z = pair x y
Axiom. (apI) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
Axiom. (apE) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
Axiom. (beta) We take the following as an axiom:
∀X : set, ∀F : set → set, ∀x : set, x ∈ X → (λx ∈ X ⇒ F x) x = F x
Axiom. (ap0_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 0) ∈ X
Axiom. (ap1_Sigma) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀z : set, z ∈ (∑x ∈ X, Y x) → (z 1) ∈ (Y (z 0))
Axiom. (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 ∈ ∏x ∈ X, Y x
Axiom. (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) ∈ (∏x ∈ X, Y x)
Axiom. (ap_Pi) We take the following as an axiom:
∀X : set, ∀Y : set → set, ∀f : set, ∀x : set, f ∈ (∏x ∈ X, Y x) → x ∈ X → f x ∈ Y x
Axiom. (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
Variable x0 x1 : set
End of Section Tuples
End of Section pair_setsum
Beginning of Section TaggedSets
End of Section TaggedSets
Beginning of Section TaggedSets2
End of Section TaggedSets2
Beginning of Section SurrealRecI
Variable F : set → (set → set) → set
Hypothesis Fr : ∀z, SNo z → ∀g h : set → set, (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set)) → (set → set)
Let G : set → (set → set → (set → set)) → set → (set → set) ≝ λalpha g ⇒ If_iii (ordinal alpha) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha)) (F z (λw ⇒ g (SNoLev w) w)) default) (λz : set ⇒ default)
Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set), (∀w ∈ SNoS_ (SNoLev z), g w = h w) → F z g = F z h
End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set) → set
Let G : set → (set → set → set) → set → (set → set) → set ≝ λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y)
End of Section SurrealRec2
Axiom. (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
Beginning of Section SurrealMinus
End of Section SurrealMinus
Beginning of Section SurrealAdd
End of Section SurrealAdd
Beginning of Section SurrealMul
Axiom. (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
Axiom. (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
Axiom. (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
Axiom. (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'
Beginning of Section mul_SNo_assoc_lems
Variable M : set → set → set
Hypothesis DL : ∀x y z, SNo x → SNo y → SNo z → x * (y + z) = x * y + x * z
Hypothesis DR : ∀x y z, SNo x → SNo y → SNo z → (x + y) * z = x * z + y * z
Hypothesis M_Lt : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u < x → v < y → u * y + x * v < x * y + u * v
Hypothesis M_Le : ∀x y u v, SNo x → SNo y → SNo u → SNo v → u ≤ x → v ≤ y → u * y + x * v ≤ x * y + u * v
Axiom. (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
Axiom. (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
End of Section SurrealMul
Beginning of Section SurrealExp
End of Section SurrealExp
Beginning of Section Int
End of Section Int
Beginning of Section SurrealAbs
End of Section SurrealAbs
Beginning of Section SNoMaxMin
End of Section SNoMaxMin
Beginning of Section DiadicRationals
End of Section DiadicRationals
Beginning of Section Reals
Axiom. (SNo_approx_real_rep) We take the following as an axiom:
∀x ∈ real, ∀p : prop, (∀f g ∈ SNoS_ ωω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, g n + - eps_ n < x) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → p) → p
End of Section Reals
Beginning of Section ComplexSNo
Beginning of Section CTaggedSets
End of Section CTaggedSets
End of Section ComplexSNo
Beginning of Section Complex
End of Section Complex