Nuprl Definition : compact-sup
compact-sup{i:l}(d;c;f) == m-sup{i:l}(d;snd(c);f;compact-mc{i:l}(d;c;f))
Definitions occuring in Statement :
compact-mc: compact-mc{i:l}(d;c;f),
m-sup: m-sup{i:l}(d;mtb;f;mc),
pi2: snd(t)
Definitions occuring in definition :
compact-mc: compact-mc{i:l}(d;c;f),
pi2: snd(t),
m-sup: m-sup{i:l}(d;mtb;f;mc)
FDL editor aliases :
compact-sup
Latex:
compact-sup\{i:l\}(d;c;f) == m-sup\{i:l\}(d;snd(c);f;compact-mc\{i:l\}(d;c;f))
Date html generated:
2019_10_30-AM-07_07_46
Last ObjectModification:
2019_10_25-PM-02_28_59
Theory : reals
Home
Index