Nuprl Definition : nearby-partitions
nearby-partitions(e;p;q) == (||p|| = ||q|| ∈ ℤ) ∧ (∀i:ℕ||p||. (|p[i] - q[i]| ≤ e))
Definitions occuring in Statement :
rleq: x ≤ y,
rabs: |x|,
rsub: x - y,
select: L[n],
length: ||as||,
int_seg: {i..j-},
all: ∀x:A. B[x],
and: P ∧ Q,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
select: L[n],
rsub: x - y,
rabs: |x|,
rleq: x ≤ y,
length: ||as||,
natural_number: $n,
int_seg: {i..j-},
all: ∀x:A. B[x],
int: ℤ,
equal: s = t ∈ T,
and: P ∧ Q
FDL editor aliases :
nearby-partitions
Latex:
nearby-partitions(e;p;q) == (||p|| = ||q||) \mwedge{} (\mforall{}i:\mBbbN{}||p||. (|p[i] - q[i]| \mleq{} e))
Date html generated:
2016_10_26-AM-09_34_02
Last ObjectModification:
2016_08_13-PM-01_32_07
Theory : reals
Home
Index