Nuprl Definition : comm
(basic):: Comm(T;op) == ∀[x,y:T]. ((x op y) = (y op x) ∈ T)
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
infix_ap: x f y,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
infix_ap: x f y
Latex:
(basic):: Comm(T;op) == \mforall{}[x,y:T]. ((x op y) = (y op x))
Date html generated:
2016_05_13-PM-04_08_51
Last ObjectModification:
2015_09_22-PM-05_45_52
Theory : fun_1
Home
Index