Nuprl Definition : range_inf
inf{f[x] | x ∈ I} == fst((TERMOF{inf-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],
inf-range-no-mc,
apply: f a,
pi1: fst(t)
TermOfs occuring in Definition :
inf-range-no-mc
FDL editor aliases :
range_inf
Latex:
inf\{f[x] | x \mmember{} I\} == fst((TERMOF\{inf-range-no-mc:o, 1:l\} I (\mlambda{}x.f[x])))
Date html generated:
2018_07_29-AM-09_42_30
Last ObjectModification:
2018_06_29-PM-04_33_39
Theory : reals
Home
Index