Nuprl Definition : bilinear
(basic)::
BiLinear(T;pl;tm) ==
∀[a,x,y:T]. (((a tm (x pl y)) = ((a tm x) pl (a tm y)) ∈ T) ∧ (((x pl y) tm a) = ((x tm a) pl (y tm a)) ∈ T))
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
infix_ap: x f y,
and: P ∧ Q,
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
Latex:
(basic)::
BiLinear(T;pl;tm) ==
\mforall{}[a,x,y:T].
(((a tm (x pl y)) = ((a tm x) pl (a tm y))) \mwedge{} (((x pl y) tm a) = ((x tm a) pl (y tm a))))
Date html generated:
2016_05_15-PM-00_02_17
Last ObjectModification:
2015_09_23-AM-06_23_45
Theory : gen_algebra_1
Home
Index