Nuprl Definition : rat-interval-third
rat-interval-third(p;I) ==
let a,b = I
in (p = ((r(2) * rat2real(a)) + rat2real(b)/r(3))) ∨ (p = (rat2real(a) + (r(2) * rat2real(b))/r(3)))
Definitions occuring in Statement :
rat2real: rat2real(q),
rdiv: (x/y),
req: x = y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
or: P ∨ Q,
spread: spread def,
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
int-to-real: r(n),
rat2real: rat2real(q),
rmul: a * b,
radd: a + b,
rdiv: (x/y),
req: x = y,
or: P ∨ Q,
spread: spread def
FDL editor aliases :
rat-interval-third
Latex:
rat-interval-third(p;I) ==
let a,b = I
in (p = ((r(2) * rat2real(a)) + rat2real(b)/r(3)))
\mvee{} (p = (rat2real(a) + (r(2) * rat2real(b))/r(3)))
Date html generated:
2019_11_04-PM-04_43_19
Last ObjectModification:
2019_11_04-PM-02_09_28
Theory : real!vectors
Home
Index