Nuprl Definition : iPolynomial
iPolynomial() == {L:iMonomial() List| ∀i:ℕ||L||. ∀j:ℕi. imonomial-less(L[j];L[i])}
Definitions occuring in Statement :
imonomial-less: imonomial-less(m1;m2),
iMonomial: iMonomial(),
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
list: T List,
iMonomial: iMonomial(),
length: ||as||,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
imonomial-less: imonomial-less(m1;m2),
select: L[n]
FDL editor aliases :
iPolynomial
Latex:
iPolynomial() == \{L:iMonomial() List| \mforall{}i:\mBbbN{}||L||. \mforall{}j:\mBbbN{}i. imonomial-less(L[j];L[i])\}
Date html generated:
2016_05_14-AM-07_00_28
Last ObjectModification:
2015_09_22-PM-05_51_43
Theory : omega
Home
Index