Nuprl Definition : req_int_terms
t1 ≡ t2 == ∀f:ℤ ⟶ ℝ. (real_term_value(f;t1) = real_term_value(f;t2))
Definitions occuring in Statement :
real_term_value: real_term_value(f;t),
req: x = y,
real: ℝ,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
int: ℤ
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
int: ℤ,
real: ℝ,
req: x = y,
real_term_value: real_term_value(f;t)
FDL editor aliases :
req_int_terms
Latex:
t1 \mequiv{} t2 == \mforall{}f:\mBbbZ{} {}\mrightarrow{} \mBbbR{}. (real\_term\_value(f;t1) = real\_term\_value(f;t2))
Date html generated:
2017_10_02-PM-07_18_16
Last ObjectModification:
2017_04_02-PM-00_38_41
Theory : reals
Home
Index