Nuprl Lemma : i-member-implies
∀I:Interval. ∀r:ℝ.
((r ∈ I)
⇒ (∃n,M:ℕ+
((r ∈ i-approx(I;n))
∧ (∀y:{y:ℝ| y ∈ I} . ((|y - r| ≤ (r1/r(M))) ⇒ (y ∈ i-approx(I;n))))
∧ (iproper(I) ⇒ iproper(i-approx(I;n))))))
Proof
Definitions occuring in Statement :
i-approx: i-approx(I;n),
i-member: r ∈ I,
iproper: iproper(I),
interval: Interval,
rdiv: (x/y),
rleq: x ≤ y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
member: t ∈ T,
nat_plus: ℕ+,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
decidable: Dec(P),
or: P ∨ Q,
uimplies: b supposing a,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
prop: ℙ,
rless: x < y,
sq_exists: ∃x:A [B[x]],
interval: Interval,
i-approx: i-approx(I;n),
i-member: r ∈ I,
iproper: iproper(I),
i-finite: i-finite(I),
right-endpoint: right-endpoint(I),
left-endpoint: left-endpoint(I),
isl: isl(x),
rccint: [l, u],
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
endpoints: endpoints(I),
outl: outl(x),
pi1: fst(t),
pi2: snd(t),
rneq: x ≠ y,
guard: {T},
bfalse: ff,
true: True,
less_than': less_than'(a;b),
less_than: a < b,
squash: ↓T,
sq_stable: SqStable(P),
cand: A c∧ B,
top: Top,
rev_uimplies: rev_uimplies(P;Q),
rge: x ≥ y,
so_apply: x[s],
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
rdiv: (x/y),
uiff: uiff(P;Q),
req_int_terms: t1 ≡ t2,
real: ℝ,
le: A ≤ B,
int_nzero: ℤ-o,
nequal: a ≠ b ∈ T ,
sq_type: SQType(T)
Latex:
\mforall{}I:Interval. \mforall{}r:\mBbbR{}.
((r \mmember{} I)
{}\mRightarrow{} (\mexists{}n,M:\mBbbN{}\msupplus{}
((r \mmember{} i-approx(I;n))
\mwedge{} (\mforall{}y:\{y:\mBbbR{}| y \mmember{} I\} . ((|y - r| \mleq{} (r1/r(M))) {}\mRightarrow{} (y \mmember{} i-approx(I;n))))
\mwedge{} (iproper(I) {}\mRightarrow{} iproper(i-approx(I;n))))))
Date html generated:
2020_05_20-AM-11_31_43
Last ObjectModification:
2020_01_06-PM-03_24_26
Theory : reals
Home
Index