Nuprl Definition : imonomial-le

imonomial-le(m1;m2) ==  snd(m1) ≤_lex snd(m2)


Definitions occuring in Statement :  intlex: l1 ≤_lex l2,  pi2: snd(t)
Definitions occuring in definition :  intlex: l1 ≤_lex l2,  pi2: snd(t)
FDL editor aliases :  imonomial-le
Latex:
imonomial-le(m1;m2)  ==    snd(m1)  \mleq{}\_lex  snd(m2)


Date html generated: 2016_05_14-AM-07_00_12
Last ObjectModification: 2015_09_22-PM-05_51_41

Theory : omega


Home Index