Nuprl Definition : alg_p
AlgP(r;a) ==
rng_p(a↓rg)
∧ IsAction(|r|;*;1;a.car;a.act)
∧ IsBilinear(|r|;a.car;a.car;+r;a.plus;a.plus;a.act)
∧ (∀p:|r|. Dist1op2opLR(a.car;a.act p;a.times))
Definitions occuring in Statement :
rng_p: rng_p(r),
rng_of_alg: a↓rg,
alg_act: a.act,
alg_times: a.times,
alg_plus: a.plus,
alg_car: a.car,
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
rng_one: 1,
rng_times: *,
rng_plus: +r,
rng_car: |r|,
dist_1op_2op_lr: Dist1op2opLR(A;1op;2op),
action_p: IsAction(A;x;e;S;f),
bilinear_p: IsBilinear(A;B;C;+a;+b;+c;f)
Definitions occuring in definition :
rng_p: rng_p(r),
rng_of_alg: a↓rg,
action_p: IsAction(A;x;e;S;f),
rng_times: *,
rng_one: 1,
and: P ∧ Q,
bilinear_p: IsBilinear(A;B;C;+a;+b;+c;f),
rng_plus: +r,
alg_plus: a.plus,
all: ∀x:A. B[x],
rng_car: |r|,
dist_1op_2op_lr: Dist1op2opLR(A;1op;2op),
alg_car: a.car,
apply: f a,
alg_act: a.act,
alg_times: a.times
Latex:
AlgP(r;a) ==
rng\_p(a\mdownarrow{}rg)
\mwedge{} IsAction(|r|;*;1;a.car;a.act)
\mwedge{} IsBilinear(|r|;a.car;a.car;+r;a.plus;a.plus;a.act)
\mwedge{} (\mforall{}p:|r|. Dist1op2opLR(a.car;a.act p;a.times))
Date html generated:
2016_05_16-AM-08_13_57
Last ObjectModification:
2015_09_23-AM-09_52_37
Theory : polynom_1
Home
Index