Nuprl Definition : sub-set
{a ∈ s | P[a]} == let T,f = s in <t:T × P[f t], λp.(f (fst(p)))>
Definitions occuring in Statement :
pi1: fst(t),
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
product: x:A × B[x]
Definitions occuring in definition :
pi1: fst(t),
apply: f a,
lambda: λx.A[x],
product: x:A × B[x],
pair: <a, b>,
spread: spread def
FDL editor aliases :
sub-set
Latex:
\{a \mmember{} s | P[a]\} == let T,f = s in <t:T \mtimes{} P[f t], \mlambda{}p.(f (fst(p)))>
Date html generated:
2018_07_29-AM-09_52_17
Last ObjectModification:
2018_07_18-AM-10_14_18
Theory : constructive!set!theory
Home
Index