Nuprl Definition : ni-eventually-equal
ni-eventually-equal(f;g) == ∃n:ℕ. ∀m:{n...}. f m = g m
Definitions occuring in Statement :
int_upper: {i...},
nat: ℕ,
bool: 𝔹,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
nat: ℕ,
all: ∀x:A. B[x],
int_upper: {i...},
equal: s = t ∈ T,
bool: 𝔹,
apply: f a
FDL editor aliases :
ni-eventually-equal
Latex:
ni-eventually-equal(f;g) == \mexists{}n:\mBbbN{}. \mforall{}m:\{n...\}. f m = g m
Date html generated:
2016_05_15-PM-01_48_50
Last ObjectModification:
2015_09_23-AM-07_37_14
Theory : basic
Home
Index