Nuprl Definition : partitions
partitions(I;p) == frs-non-dec(p) ∧ (0 < ||p|| ⇒ ((left-endpoint(I) ≤ p[0]) ∧ (last(p) ≤ right-endpoint(I))))
Definitions occuring in Statement :
frs-non-dec: frs-non-dec(L),
right-endpoint: right-endpoint(I),
left-endpoint: left-endpoint(I),
rleq: x ≤ y,
last: last(L),
select: L[n],
length: ||as||,
less_than: a < b,
implies: P ⇒ Q,
and: P ∧ Q,
natural_number: $n
Definitions occuring in definition :
frs-non-dec: frs-non-dec(L),
implies: P ⇒ Q,
less_than: a < b,
length: ||as||,
and: P ∧ Q,
left-endpoint: left-endpoint(I),
select: L[n],
natural_number: $n,
rleq: x ≤ y,
last: last(L),
right-endpoint: right-endpoint(I)
FDL editor aliases :
partitions
partitions
Latex:
partitions(I;p) ==
frs-non-dec(p) \mwedge{} (0 < ||p|| {}\mRightarrow{} ((left-endpoint(I) \mleq{} p[0]) \mwedge{} (last(p) \mleq{} right-endpoint(I))))
Date html generated:
2016_05_18-AM-08_54_45
Last ObjectModification:
2015_09_23-AM-09_08_52
Theory : reals
Home
Index