Nuprl Definition : proj-eq

a = b ==  ∀i,j:ℕn + 1.  (((a i) * (b j)) = ((b i) * (a j)))


Definitions occuring in Statement :  req: x = y,  rmul: a * b,  int_seg: {i..j-},  all: ∀x:A. B[x],  apply: f a,  add: n + m,  natural_number: $n
Definitions occuring in definition :  all: ∀x:A. B[x],  int_seg: {i..j-},  add: n + m,  natural_number: $n,  req: x = y,  rmul: a * b,  apply: f a
FDL editor aliases :  proj-eq
Latex:
a  =  b  ==    \mforall{}i,j:\mBbbN{}n  +  1.    (((a  i)  *  (b  j))  =  ((b  i)  *  (a  j)))


Date html generated: 2017_10_05-AM-00_17_59
Last ObjectModification: 2017_06_17-AM-10_07_10

Theory : inner!product!spaces


Home Index