Nuprl Definition : action_p
(basic):: IsAction(A;x;e;S;f) == (∀[a,b:A]. ∀u:S. (((a x b) f u) = (a f (b f u)) ∈ S)) ∧ (∀[u:S]. ((e f u) = u ∈ S))
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
infix_ap: x f y,
all: ∀x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
infix_ap: x f y
Latex:
(basic)::
IsAction(A;x;e;S;f) ==
(\mforall{}[a,b:A]. \mforall{}u:S. (((a x b) f u) = (a f (b f u)))) \mwedge{} (\mforall{}[u:S]. ((e f u) = u))
Date html generated:
2016_05_15-PM-00_02_32
Last ObjectModification:
2015_09_23-AM-06_23_47
Theory : gen_algebra_1
Home
Index