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