Nuprl Definition : real-vec-be
real-vec-be(n;a;b;c) == ∃t:ℝ. ((t ∈ [r0, r1]) ∧ req-vec(n;b;t*a + r1 - t*c))
Definitions occuring in Statement :
real-vec-mul: a*X,
real-vec-add: X + Y,
req-vec: req-vec(n;x;y),
rccint: [l, u],
i-member: r ∈ I,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
exists: ∃x:A. B[x],
and: P ∧ Q,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
int-to-real: r(n),
rsub: x - y,
real-vec-mul: a*X,
real-vec-add: X + Y,
req-vec: req-vec(n;x;y),
rccint: [l, u],
i-member: r ∈ I,
and: P ∧ Q,
real: ℝ,
exists: ∃x:A. B[x]
FDL editor aliases :
real-vec-be
Latex:
real-vec-be(n;a;b;c) == \mexists{}t:\mBbbR{}. ((t \mmember{} [r0, r1]) \mwedge{} req-vec(n;b;t*a + r1 - t*c))
Date html generated:
2016_10_26-AM-10_20_09
Last ObjectModification:
2016_09_26-PM-00_07_09
Theory : reals
Home
Index