Nuprl Definition : cancel
(basic):: Cancel(T;S;op) == ∀[u,v:T]. ∀[w:S]. u = v ∈ T supposing (w op u) = (w op v) ∈ T
Definitions occuring in Statement :
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
infix_ap: x f y,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
infix_ap: x f y,
equal: s = t ∈ T
Latex:
(basic):: Cancel(T;S;op) == \mforall{}[u,v:T]. \mforall{}[w:S]. u = v supposing (w op u) = (w op v)
Date html generated:
2016_05_15-PM-00_02_52
Last ObjectModification:
2015_09_23-AM-06_23_56
Theory : gen_algebra_1
Home
Index