Nuprl Definition : bilinear

Nuprl Definition : bilinear_p

(basic)::
IsBilinear(A;B;C;+a;+b;+c;f) ==
(∀[a1,a2:A]. ∀[b:B]. (((a1 +a a2) f b) = ((a1 f b) +c (a2 f b)) ∈ C))
∧ (∀[a:A]. ∀[b1,b2:B]. ((a f (b1 +b b2)) = ((a f b1) +c (a f b2)) ∈ C))

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 : and: P ∧ Q, uall: ∀[x:A]. B[x], equal: s = t ∈ T, infix_ap: x f y

Latex:
(basic):: IsBilinear(A;B;C;+a;+b;+c;f) == (\mforall{}[a1,a2:A]. \mforall{}[b:B]. (((a1 +a a2) f b) = ((a1 f b) +c (a2 f b)))) \mwedge{} (\mforall{}[a:A]. \mforall{}[b1,b2:B]. ((a f (b1 +b b2)) = ((a f b1) +c (a f b2)))) Date html generated: 2016_05_15-PM-00_02_26 Last ObjectModification: 2015_09_23-AM-06_23_46 Theory : gen_algebra_1 Home Index