Nuprl Definition : fun_thru_2op
(basic):: FunThru2op(A;B;opa;opb;f) == ∀[a1,a2:A]. ((f (a1 opa a2)) = ((f a1) opb (f a2)) ∈ B)
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
infix_ap: x f y,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
infix_ap: x f y,
apply: f a
Latex:
(basic):: FunThru2op(A;B;opa;opb;f) == \mforall{}[a1,a2:A]. ((f (a1 opa a2)) = ((f a1) opb (f a2)))
Date html generated:
2016_05_15-PM-00_02_47
Last ObjectModification:
2015_09_23-AM-06_23_51
Theory : gen_algebra_1
Home
Index