Nuprl Definition : eqfun_p
(basic):: IsEqFun(T;eq) == ∀[x,y:T]. uiff(↑(x eq y);x = y ∈ T)
Definitions occuring in Statement :
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
infix_ap: x f y,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
uiff: uiff(P;Q),
assert: ↑b,
infix_ap: x f y,
equal: s = t ∈ T
FDL editor aliases :
eqfun_p
Latex:
(basic):: IsEqFun(T;eq) == \mforall{}[x,y:T]. uiff(\muparrow{}(x eq y);x = y)
Date html generated:
2016_05_13-PM-04_15_42
Last ObjectModification:
2015_09_22-PM-05_46_04
Theory : rel_1
Home
Index