Nuprl Definition : req_rat_term
r ≡ p/q ==
∀f:ℤ ⟶ ℝ
let P,x = rat_term_to_real(f;r)
in P ⇒ (real_term_value(f;q) ≠ r0 ∧ (x = (real_term_value(f;p)/real_term_value(f;q))))
Definitions occuring in Statement :
rat_term_to_real: rat_term_to_real(f;t),
rdiv: (x/y),
rneq: x ≠ y,
real_term_value: real_term_value(f;t),
req: x = y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
spread: spread def,
natural_number: $n,
int: ℤ
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
int: ℤ,
real: ℝ,
spread: spread def,
rat_term_to_real: rat_term_to_real(f;t),
implies: P ⇒ Q,
and: P ∧ Q,
rneq: x ≠ y,
int-to-real: r(n),
natural_number: $n,
req: x = y,
rdiv: (x/y),
real_term_value: real_term_value(f;t)
FDL editor aliases :
req_rat_term
Latex:
r \mequiv{} p/q ==
\mforall{}f:\mBbbZ{} {}\mrightarrow{} \mBbbR{}
let P,x = rat\_term\_to\_real(f;r)
in P {}\mRightarrow{} (real\_term\_value(f;q) \mneq{} r0 \mwedge{} (x = (real\_term\_value(f;p)/real\_term\_value(f;q))))
Date html generated:
2019_10_29-AM-09_40_41
Last ObjectModification:
2019_04_01-AM-10_49_27
Theory : reals
Home
Index