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