Nuprl Lemma : mesh-property
∀I:Interval
(icompact(I)
⇒ (∀p:partition(I). ∀e:ℝ.
((r0 < e)
⇒ ∀x:ℝ. ((x ∈ I) ⇒ (∃i:ℕ||full-partition(I;p)||. (|x - full-partition(I;p)[i]| ≤ e)))
supposing partition-mesh(I;p) ≤ e)))
Proof
Definitions occuring in Statement :
partition-mesh: partition-mesh(I;p),
full-partition: full-partition(I;p),
partition: partition(I),
icompact: icompact(I),
i-member: r ∈ I,
interval: Interval,
rleq: x ≤ y,
rless: x < y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
select: L[n],
length: ||as||,
int_seg: {i..j-},
uimplies: b supposing a,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uimplies: b supposing a,
member: t ∈ T,
rleq: x ≤ y,
rnonneg: rnonneg(x),
uall: ∀[x:A]. B[x],
le: A ≤ B,
and: P ∧ Q,
full-partition: full-partition(I;p),
rless: x < y,
sq_exists: ∃x:A [B[x]],
nat_plus: ℕ+,
decidable: Dec(P),
or: P ∨ Q,
partition: partition(I),
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
prop: ℙ,
guard: {T},
uiff: uiff(P;Q),
int_seg: {i..j-},
lelt: i ≤ j < k,
subtype_rel: A ⊆r B,
real: ℝ,
sq_stable: SqStable(P),
squash: ↓T,
sq_type: SQType(T),
cand: A c∧ B,
ge: i ≥ j ,
nat: ℕ,
less_than': less_than'(a;b),
true: True,
select: L[n],
cons: [a / b],
subtract: n - m,
less_than: a < b,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
icompact: icompact(I),
last: last(L),
so_lambda: λ2x.t[x],
so_apply: x[s],
append: as @ bs,
list_ind: list_ind,
nil: [],
it: ⋅,
right-endpoint: right-endpoint(I),
pi2: snd(t),
endpoints: endpoints(I),
left-endpoint: left-endpoint(I),
pi1: fst(t),
rbetween: x≤y≤z
Latex:
\mforall{}I:Interval
(icompact(I)
{}\mRightarrow{} (\mforall{}p:partition(I). \mforall{}e:\mBbbR{}.
((r0 < e)
{}\mRightarrow{} \mforall{}x:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} (\mexists{}i:\mBbbN{}||full-partition(I;p)||. (|x - full-partition(I;p)[i]| \mleq{} e)))
supposing partition-mesh(I;p) \mleq{} e)))
Date html generated:
2020_05_20-AM-11_37_43
Last ObjectModification:
2019_12_28-PM-09_01_42
Theory : reals
Home
Index