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.
Primitive. The name
real is a term of type
set.
Primitive. The name
rational is a term of type
set.
L27Axiom. (
real_I) We take the following as an axiom:
∀x ∈ SNoS_ (ordsucc ω), x ≠ ω → x ≠ - ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → x ∈ real
L28Axiom. (
real_E) We take the following as an axiom:
∀x ∈ real, ∀p : prop, (SNo x → SNoLev x ∈ ordsucc ω → x ∈ SNoS_ (ordsucc ω) → - ω < x → x < ω → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → p) → p
L29Axiom. (
real_SNo) We take the following as an axiom:
L32Axiom. (
real_0) We take the following as an axiom:
L33Axiom. (
real_1) We take the following as an axiom:
L35Axiom. (
real_SNoCut_SNoS_omega) We take the following as an axiom:
∀L R ⊆ SNoS_ ω, SNoCutP L R → L ≠ 0 → R ≠ 0 → (∀w ∈ L, ∃w' ∈ L, w < w') → (∀z ∈ R, ∃z' ∈ R, z' < z) → SNoCut L R ∈ real
L36Axiom. (
real_SNoCut) We take the following as an axiom:
∀L R ⊆ real, SNoCutP L R → L ≠ 0 → R ≠ 0 → (∀w ∈ L, ∃w' ∈ L, w < w') → (∀z ∈ R, ∃z' ∈ R, z' < z) → SNoCut L R ∈ real
L37Axiom. (
minus_SNo_prereal_1) We take the following as an axiom:
∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - - x) < eps_ k) → q = - x)
L38Axiom. (
minus_SNo_prereal_2) We take the following as an axiom:
∀x, SNo x → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < - x ∧ - x < q + eps_ k)
L39Axiom. (
SNo_prereal_incr_lower_pos) We take the following as an axiom:
∀x, SNo x → 0 < x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∀k ∈ ω, ∀p : prop, (∀q ∈ SNoS_ ω, 0 < q → q < x → x < q + eps_ k → p) → p
L41Axiom. (
SNo_prereal_incr_lower_approx) We take the following as an axiom:
∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃f ∈ SNoS_ ωω, ∀n ∈ ω, f n < x ∧ x < f n + eps_ n ∧ ∀i ∈ n, f i < f n
L42Axiom. (
SNo_prereal_decr_upper_approx) We take the following as an axiom:
∀x, SNo x → (∀q ∈ SNoS_ ω, (∀k ∈ ω, abs_SNo (q + - x) < eps_ k) → q = x) → (∀k ∈ ω, ∃q ∈ SNoS_ ω, q < x ∧ x < q + eps_ k) → ∃g ∈ SNoS_ ωω, ∀n ∈ ω, g n + - eps_ n < x ∧ x < g n ∧ ∀i ∈ n, g n < g i
L43Axiom. (
SNoCutP_SNoCut_lim) We take the following as an axiom:
∀lambda, ordinal lambda → (∀alpha ∈ lambda, ordsucc alpha ∈ lambda) → ∀L R ⊆ SNoS_ lambda, SNoCutP L R → SNoLev (SNoCut L R) ∈ ordsucc lambda
L44Axiom. (
SNoCutP_SNoCut_omega) We take the following as an axiom:
∀L R ⊆ SNoS_ ω, SNoCutP L R → SNoLev (SNoCut L R) ∈ ordsucc ω
L45Axiom. (
SNo_approx_real_lem) We take the following as an axiom:
∀f g ∈ SNoS_ ωω, (∀n m ∈ ω, f n < g m) → ∀p : prop, (SNoCutP {f n|n ∈ ω} {g n|n ∈ ω} → SNo (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → SNoLev (SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) ∈ ordsucc ω → SNoCut {f n|n ∈ ω} {g n|n ∈ ω} ∈ SNoS_ (ordsucc ω) → (∀n ∈ ω, f n < SNoCut {f n|n ∈ ω} {g n|n ∈ ω}) → (∀n ∈ ω, SNoCut {f n|n ∈ ω} {g n|n ∈ ω} < g n) → p) → p
L46Axiom. (
SNo_approx_real) We take the following as an axiom:
∀x, SNo x → ∀f g ∈ SNoS_ ωω, (∀n ∈ ω, f n < x) → (∀n ∈ ω, x < f n + eps_ n) → (∀n ∈ ω, ∀i ∈ n, f i < f n) → (∀n ∈ ω, x < g n) → (∀n ∈ ω, ∀i ∈ n, g n < g i) → x = SNoCut {f n|n ∈ ω} {g n|n ∈ ω} → x ∈ real
L47Axiom. (
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
L52Axiom. (
abs_SNo_intvl_bd) We take the following as an axiom:
∀x y z, SNo x → SNo y → SNo z → x ≤ y → y < x + z → abs_SNo (y + - x) < z
L55Axiom. (
real_recip_SNo_lem1) We take the following as an axiom:
∀x, SNo x → x ∈ real → 0 < x → recip_SNo_pos x ∈ real ∧ ∀k, nat_p k → (SNo_recipaux x recip_SNo_pos k 0 ⊆ real) ∧ (SNo_recipaux x recip_SNo_pos k 1 ⊆ real)
L59Axiom. (
sqrt_SNo_nonneg_0inL0) We take the following as an axiom:
∀x, SNo x → 0 ≤ x → 0 ∈ SNoLev x → 0 ∈ SNo_sqrtaux x sqrt_SNo_nonneg 0 0
L60Axiom. (
sqrt_SNo_nonneg_Lnonempty) We take the following as an axiom:
∀x, SNo x → 0 ≤ x → 0 ∈ SNoLev x → (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 0) ≠ 0
L61Axiom. (
sqrt_SNo_nonneg_Rnonempty) We take the following as an axiom:
∀x, SNo x → 0 ≤ x → 1 ∈ SNoLev x → (⋃k ∈ ωSNo_sqrtaux x sqrt_SNo_nonneg k 1) ≠ 0
L67Axiom. (
real_complete1) We take the following as an axiom:
∀a b ∈ realω, (∀n ∈ ω, a n ≤ b n ∧ a n ≤ a (ordsucc n) ∧ b (ordsucc n) ≤ b n) → ∃x ∈ real, ∀n ∈ ω, a n ≤ x ∧ x ≤ b n
L68Axiom. (
real_complete2) We take the following as an axiom:
∀a b ∈ realω, (∀n ∈ ω, a n ≤ b n ∧ a n ≤ a (n + 1) ∧ b (n + 1) ≤ b n) → ∃x ∈ real, ∀n ∈ ω, a n ≤ x ∧ x ≤ b n
End of Section Reals