Nuprl Definition : rational-vec
rational-vec(n;x) ==  ∀i:ℕn. ∃d:ℕ+. ∃n:ℤ. ((x i) = (r(n)/r(d)))
Definitions occuring in Statement : 
rdiv: (x/y)
, 
req: x = y
, 
int-to-real: r(n)
, 
int_seg: {i..j-}
, 
nat_plus: ℕ+
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
apply: f a
, 
natural_number: $n
, 
int: ℤ
Definitions occuring in definition : 
all: ∀x:A. B[x]
, 
int_seg: {i..j-}
, 
natural_number: $n
, 
nat_plus: ℕ+
, 
exists: ∃x:A. B[x]
, 
int: ℤ
, 
req: x = y
, 
apply: f a
, 
rdiv: (x/y)
, 
int-to-real: r(n)
FDL editor aliases : 
rational-vec
Latex:
rational-vec(n;x)  ==    \mforall{}i:\mBbbN{}n.  \mexists{}d:\mBbbN{}\msupplus{}.  \mexists{}n:\mBbbZ{}.  ((x  i)  =  (r(n)/r(d)))
Date html generated:
2019_10_30-AM-10_14_41
Last ObjectModification:
2019_06_28-PM-01_52_06
Theory : real!vectors
Home
Index