Nuprl Definition : dist_1op_2op_lr
(basic)::
Dist1op2opLR(A;1op;2op) ==
∀[u,v:A]. (((1op (u 2op v)) = ((1op u) 2op v) ∈ A) ∧ ((1op (u 2op v)) = (u 2op (1op v)) ∈ A))
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
infix_ap: x f y,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
and: P ∧ Q,
equal: s = t ∈ T,
infix_ap: x f y,
apply: f a
Latex:
(basic)::
Dist1op2opLR(A;1op;2op) ==
\mforall{}[u,v:A]. (((1op (u 2op v)) = ((1op u) 2op v)) \mwedge{} ((1op (u 2op v)) = (u 2op (1op v))))
Date html generated:
2016_05_15-PM-00_02_37
Last ObjectModification:
2015_09_23-AM-06_23_49
Theory : gen_algebra_1
Home
Index