Nuprl Definition : range-sup
sup{f[x]|x ∈ I} == fst((TERMOF{sup-range:o, 1:l} I (λx.f[x]) mc))
Definitions occuring in Statement :
pi1: fst(t),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
pi1: fst(t),
apply: f a,
lambda: λx.A[x]
TermOfs occuring in Definition :
sup-range
FDL editor aliases :
range-sup
Latex:
sup\{f[x]|x \mmember{} I\} == fst((TERMOF\{sup-range:o, 1:l\} I (\mlambda{}x.f[x]) mc))
Date html generated:
2016_05_18-AM-09_15_49
Last ObjectModification:
2015_09_23-AM-09_10_20
Theory : reals
Home
Index