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