Nuprl Definition : range-inf
inf{f[x]|x ∈ I} == fst((TERMOF{inf-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 :
inf-range
FDL editor aliases :
range-inf
Latex:
inf\{f[x]|x \mmember{} I\} == fst((TERMOF\{inf-range:o, 1:l\} I (\mlambda{}x.f[x]) mc))
Date html generated:
2016_05_18-AM-09_16_21
Last ObjectModification:
2015_09_23-AM-09_10_26
Theory : reals
Home
Index