Nuprl Definition : m-sup
m-sup{i:l}(d;mtb;f;mc) == fst(snd((TERMOF{m-TB-sup-and-inf:o, 1:l, i:l} d mtb f mc)))
Definitions occuring in Statement :
pi1: fst(t),
pi2: snd(t),
apply: f a
Definitions occuring in definition :
m-TB-sup-and-inf,
apply: f a,
pi2: snd(t),
pi1: fst(t)
TermOfs occuring in Definition :
m-TB-sup-and-inf
FDL editor aliases :
m-sup
Latex:
m-sup\{i:l\}(d;mtb;f;mc) == fst(snd((TERMOF\{m-TB-sup-and-inf:o, 1:l, i:l\} d mtb f mc)))
Date html generated:
2019_10_30-AM-06_54_03
Last ObjectModification:
2019_10_25-PM-00_57_01
Theory : reals
Home
Index