Nuprl Definition : mfun-class
mfun-class(X;dx;Y;dy) == f,g:FUN(X ⟶ Y)//meqfun(dy;X;f;g)
Definitions occuring in Statement :
meqfun: meqfun(d;A;f;g),
mfun: FUN(X ⟶ Y),
quotient: x,y:A//B[x; y]
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
mfun: FUN(X ⟶ Y),
meqfun: meqfun(d;A;f;g)
FDL editor aliases :
mfun-class
Latex:
mfun-class(X;dx;Y;dy) == f,g:FUN(X {}\mrightarrow{} Y)//meqfun(dy;X;f;g)
Date html generated:
2019_10_30-AM-06_32_48
Last ObjectModification:
2019_10_02-AM-10_06_36
Theory : reals
Home
Index