Nuprl Definition : mcomplete
mcomplete(M) == let X,d = M in ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
Definitions occuring in Statement :
mconverges: x[n]↓ as n→∞,
mcauchy: mcauchy(d;n.x[n]),
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
spread: spread def
Definitions occuring in definition :
spread: spread def,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
implies: P ⇒ Q,
mcauchy: mcauchy(d;n.x[n]),
mconverges: x[n]↓ as n→∞,
apply: f a
FDL editor aliases :
mcomplete
Latex:
mcomplete(M) == let X,d = M in \mforall{}x:\mBbbN{} {}\mrightarrow{} X. (mcauchy(d;n.x n) {}\mRightarrow{} x n\mdownarrow{} as n\mrightarrow{}\minfty{})
Date html generated:
2019_10_30-AM-06_41_50
Last ObjectModification:
2019_10_02-AM-10_54_27
Theory : reals
Home
Index