Nuprl Definition : module_hom_p
(compound)::
module_hom_p(a; m; n; f) ==
FunThru2op(m.car;n.car;m.plus;n.plus;f) ∧ (∀u:|a|. fun_thru_1op(m.car;n.car;m.act u;n.act u;f))
Definitions occuring in Statement :
alg_act: a.act,
alg_plus: a.plus,
alg_car: a.car,
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
rng_car: |r|,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
fun_thru_1op: fun_thru_1op(A;B;opa;opb;f)
Definitions occuring in definition :
and: P ∧ Q,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
alg_plus: a.plus,
all: ∀x:A. B[x],
rng_car: |r|,
fun_thru_1op: fun_thru_1op(A;B;opa;opb;f),
alg_car: a.car,
apply: f a,
alg_act: a.act
Latex:
(compound)::
module\_hom\_p(a; m; n; f) ==
FunThru2op(m.car;n.car;m.plus;n.plus;f) \mwedge{} (\mforall{}u:|a|. fun\_thru\_1op(m.car;n.car;m.act u;n.act u;f))
Date html generated:
2016_05_16-AM-07_27_03
Last ObjectModification:
2015_09_23-AM-09_51_01
Theory : algebras_1
Home
Index