Nuprl Lemma : adjacent-partition-points
∀[I:Interval]
∀[p:partition(I)]
(((¬0 < ||p||) ⇒ r0≤right-endpoint(I) - left-endpoint(I)≤partition-mesh(I;p))
∧ (0 < ||p||
⇒ (r0≤p[0] - left-endpoint(I)≤partition-mesh(I;p)
∧ (∀i:ℕ||p|| - 1. r0≤p[i + 1] - p[i]≤partition-mesh(I;p))
∧ r0≤right-endpoint(I) - last(p)≤partition-mesh(I;p))))
supposing icompact(I)
Proof
Definitions occuring in Statement :
partition-mesh: partition-mesh(I;p),
partition: partition(I),
icompact: icompact(I),
right-endpoint: right-endpoint(I),
left-endpoint: left-endpoint(I),
interval: Interval,
rbetween: x≤y≤z,
rsub: x - y,
int-to-real: r(n),
last: last(L),
select: L[n],
length: ||as||,
int_seg: {i..j-},
less_than: a < b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
partition-mesh: partition-mesh(I;p),
all: ∀x:A. B[x],
full-partition: full-partition(I;p),
int_seg: {i..j-},
lelt: i ≤ j < k,
and: P ∧ Q,
partition: partition(I),
decidable: Dec(P),
or: P ∨ Q,
false: False,
less_than: a < b,
squash: ↓T,
uiff: uiff(P;Q),
not: ¬A,
implies: P ⇒ Q,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
prop: ℙ,
rbetween: x≤y≤z,
rleq: x ≤ y,
rnonneg: rnonneg(x),
le: A ≤ B,
icompact: icompact(I),
less_than': less_than'(a;b),
nat_plus: ℕ+,
guard: {T},
select: L[n],
cons: [a / b],
subtract: n - m,
ge: i ≥ j ,
true: True,
so_apply: x[s1;s2;s3],
top: Top,
so_lambda: so_lambda3,
append: as @ bs,
subtype_rel: A ⊆r B,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
real: ℝ,
int_iseg: {i...j},
so_lambda: λ2x.t[x],
so_apply: x[s],
last: last(L)
Latex:
\mforall{}[I:Interval]
\mforall{}[p:partition(I)]
(((\mneg{}0 < ||p||) {}\mRightarrow{} r0\mleq{}right-endpoint(I) - left-endpoint(I)\mleq{}partition-mesh(I;p))
\mwedge{} (0 < ||p||
{}\mRightarrow{} (r0\mleq{}p[0] - left-endpoint(I)\mleq{}partition-mesh(I;p)
\mwedge{} (\mforall{}i:\mBbbN{}||p|| - 1. r0\mleq{}p[i + 1] - p[i]\mleq{}partition-mesh(I;p))
\mwedge{} r0\mleq{}right-endpoint(I) - last(p)\mleq{}partition-mesh(I;p))))
supposing icompact(I)
Date html generated:
2020_05_20-AM-11_37_20
Last ObjectModification:
2020_01_02-PM-01_30_05
Theory : reals
Home
Index