Nuprl Lemma : reals-close-or-rneq-ext
∀K:ℕ+
(∃g:ℝ ⟶ ℝ ⟶ ℕ3 [(∀x,y:ℝ.
((((g x y) = 1 ∈ ℤ) ⇒ ((r1/r(K)) < (y - x)))
∧ (((g x y) = 2 ∈ ℤ) ⇒ ((r1/r(K)) < (x - y)))
∧ (((g x y) = 0 ∈ ℤ) ⇒ (|x - y| < (r(2)/r(K))))))])
Proof
Definitions occuring in Statement :
rdiv: (x/y),
rless: x < y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
int_seg: {i..j-},
nat_plus: ℕ+,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
rabs: |x|,
rless-case: rless-case(x;y;n;z),
rminus: -(x),
le_int: i ≤z j,
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
btrue: tt,
it: ⋅,
bfalse: ff,
imax: imax(a;b),
experimental: experimental{impliesFunctionality}(possibleextract),
rclose-or-sep: rclose-or-sep(K;x;y),
uall: ∀[x:A]. B[x],
top: Top,
uimplies: b supposing a,
all: ∀x:A. B[x],
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
implies: P ⇒ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
prop: ℙ,
false: False,
sq_type: SQType(T),
guard: {T},
reals-close-or-rneq,
rless_functionality,
rabs-difference-lower-bound,
rless-iff4,
rless-iff-large-diff,
rmax_strict_ub,
iff_weakening_equal,
radd-preserves-rless,
regular-less-iff,
decidable__le,
any: any x,
rless-iff2,
bool_cases,
radd_functionality_wrt_rless1,
rless-iff-rpositive,
rpositive_functionality,
rpositive-radd2,
rpositive-iff,
rpositive2_functionality,
bdd-diff_inversion,
accelerate-bdd-diff,
rnonneg-iff,
imax_lb,
bdd-diff-equiv,
le_functionality,
so_lambda: so_lambda4,
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x.t[x],
so_apply: x[s]
Latex:
\mforall{}K:\mBbbN{}\msupplus{}
(\mexists{}g:\mBbbR{} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbN{}3 [(\mforall{}x,y:\mBbbR{}.
((((g x y) = 1) {}\mRightarrow{} ((r1/r(K)) < (y - x)))
\mwedge{} (((g x y) = 2) {}\mRightarrow{} ((r1/r(K)) < (x - y)))
\mwedge{} (((g x y) = 0) {}\mRightarrow{} (|x - y| < (r(2)/r(K))))))])
Date html generated:
2020_05_20-AM-11_06_01
Last ObjectModification:
2020_03_19-PM-01_16_39
Theory : reals
Home
Index