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: y int-to-real: r(n) int_seg: {i..j-} nat_plus: + all: x:A. B[x] exists: x:A. B[x] apply: 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: y apply: 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