Nuprl Definition : is-partition-choice
is-partition-choice(p;x) == ∀i:ℕ||p|| - 1. (x i ∈ [p[i], p[i + 1]])
Definitions occuring in Statement :
rccint: [l, u],
i-member: r ∈ I,
select: L[n],
length: ||as||,
int_seg: {i..j-},
all: ∀x:A. B[x],
apply: f a,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
int_seg: {i..j-},
subtract: n - m,
length: ||as||,
i-member: r ∈ I,
rccint: [l, u],
select: L[n],
add: n + m,
natural_number: $n,
apply: f a
FDL editor aliases :
is-partition-choice
Latex:
is-partition-choice(p;x) == \mforall{}i:\mBbbN{}||p|| - 1. (x i \mmember{} [p[i], p[i + 1]])
Date html generated:
2016_05_18-AM-09_03_02
Last ObjectModification:
2015_09_23-AM-09_09_36
Theory : reals
Home
Index