Nuprl Definition : real-vec-between
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),
rooint: (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),
rooint: (l, u),
i-member: r ∈ I,
and: P ∧ Q,
real: ℝ,
exists: ∃x:A. B[x]
FDL editor aliases :
real-vec-between
Latex:
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_17_19
Last ObjectModification:
2016_09_24-PM-09_26_26
Theory : reals
Home
Index