Nuprl Definition : equiv_int_terms
t1 ≡ t2 == ∀f:ℤ ⟶ ℤ. (int_term_value(f;t1) = int_term_value(f;t2) ∈ ℤ)
Definitions occuring in Statement :
int_term_value: int_term_value(f;t),
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
equal: s = t ∈ T,
int: ℤ,
int_term_value: int_term_value(f;t)
FDL editor aliases :
equiv_int_terms
Latex:
t1 \mequiv{} t2 == \mforall{}f:\mBbbZ{} {}\mrightarrow{} \mBbbZ{}. (int\_term\_value(f;t1) = int\_term\_value(f;t2))
Date html generated:
2016_05_14-AM-06_59_42
Last ObjectModification:
2015_09_22-PM-05_51_38
Theory : omega
Home
Index