Nuprl Definition : per-set
per-set(A;a.B[a]) == pertype(λa,b. ((a = b ∈ A) ∧ B[a]))
Definitions occuring in Statement :
pertype: pertype(R),
and: P ∧ Q,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
pertype: pertype(R),
lambda: λx.A[x],
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
per-set
Latex:
per-set(A;a.B[a]) == pertype(\mlambda{}a,b. ((a = b) \mwedge{} B[a]))
Date html generated:
2016_05_13-PM-03_54_28
Last ObjectModification:
2015_09_22-PM-05_45_33
Theory : per!type
Home
Index