Nuprl Definition : pv11_p1_in_domain
pv11_p1_in_domain(Cmd) == λx,xys. x ∈b map(λx.(fst(x));xys))
Definitions occuring in Statement :
deq-member: x ∈b L),
int-deq: IntDeq,
map: map(f;as),
pi1: fst(t),
lambda: λx.A[x]
FDL editor aliases :
pv11_p1_in_domain
Latex:
pv11\_p1\_in\_domain(Cmd) == \mlambda{}x,xys. x \mmember{}\msubb{} map(\mlambda{}x.(fst(x));xys))
Date html generated:
2015_07_23-PM-04_11_21
Last ObjectModification:
2014_11_26-AM-11_22_48
Home
Index