Nuprl Definition : fun_thru_1op
(basic):: fun_thru_1op(A;B;opa;opb;f) == ∀[a:A]. ((f (opa a)) = (opb (f a)) ∈ B)
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
apply: f a
Latex:
(basic):: fun\_thru\_1op(A;B;opa;opb;f) == \mforall{}[a:A]. ((f (opa a)) = (opb (f a)))
Date html generated:
2016_05_15-PM-00_02_41
Last ObjectModification:
2015_09_23-AM-06_23_50
Theory : gen_algebra_1
Home
Index