Nuprl Definition : assoc
(basic):: Assoc(T;op) == ∀[x,y,z:T]. ((x op (y op z)) = ((x op y) op z) ∈ 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):: Assoc(T;op) == \mforall{}[x,y,z:T]. ((x op (y op z)) = ((x op y) op z))
Date html generated:
2016_05_13-PM-04_08_45
Last ObjectModification:
2015_09_22-PM-05_45_51
Theory : fun_1
Home
Index