Nuprl Definition : Piset
Πa:A.B[a] == {g ∈ piset(A;a.B[a]) | singlevalued-graph(A;a.B[a];g)}
Definitions occuring in Statement :
singlevalued-graph: singlevalued-graph(A;a.B[a];grph),
piset: piset(A;a.B[a]),
sub-set: {a ∈ s | P[a]}
Definitions occuring in definition :
singlevalued-graph: singlevalued-graph(A;a.B[a];grph),
piset: piset(A;a.B[a]),
sub-set: {a ∈ s | P[a]}
FDL editor aliases :
Piset
Latex:
\mPi{}a:A.B[a] == \{g \mmember{} piset(A;a.B[a]) | singlevalued-graph(A;a.B[a];g)\}
Date html generated:
2018_05_29-PM-01_50_48
Last ObjectModification:
2018_05_26-PM-08_37_21
Theory : constructive!set!theory
Home
Index