Nuprl Definition : partition-choice
partition-choice(p) == i:ℕ||p|| - 1 ⟶ {x:ℝ| x ∈ [p[i], p[i + 1]]}
Definitions occuring in Statement :
rccint: [l, u],
i-member: r ∈ I,
real: ℝ,
select: L[n],
length: ||as||,
int_seg: {i..j-},
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
function: x:A ⟶ B[x],
int_seg: {i..j-},
subtract: n - m,
length: ||as||,
set: {x:A| B[x]} ,
real: ℝ,
i-member: r ∈ I,
rccint: [l, u],
select: L[n],
add: n + m,
natural_number: $n
FDL editor aliases :
partition-choice
partition-choice
Latex:
partition-choice(p) == i:\mBbbN{}||p|| - 1 {}\mrightarrow{} \{x:\mBbbR{}| x \mmember{} [p[i], p[i + 1]]\}
Date html generated:
2016_05_18-AM-09_03_34
Last ObjectModification:
2015_09_23-AM-09_09_44
Theory : reals
Home
Index