Nuprl Definition : equiv-class
equiv-class(A;a,b.E[a; b];t) == {b:A| ↑E[t; b]}
Definitions occuring in Statement :
assert: ↑b,
set: {x:A| B[x]}
Definitions occuring in definition :
assert: ↑b,
set: {x:A| B[x]}
FDL editor aliases :
equiv-class
Latex:
equiv-class(A;a,b.E[a; b];t) == \{b:A| \muparrow{}E[t; b]\}
Date html generated:
2016_10_21-AM-09_43_48
Last ObjectModification:
2016_08_07-PM-05_56_55
Theory : quot_1
Home
Index