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