Nuprl Lemma : reals-complete
mcomplete(ℝ with rmetric())
Proof
Definitions occuring in Statement :
mcomplete: mcomplete(M),
mk-metric-space: X with d,
rmetric: rmetric(),
real: ℝ
Definitions unfolded in proof :
rmetric: rmetric(),
mcomplete: mcomplete(M),
mk-metric-space: X with d,
mconverges: x[n]↓ as n→∞,
mcauchy: mcauchy(d;n.x[n]),
mconverges-to: lim n→∞.x[n] = y,
mdist: mdist(d;x;y),
converges-to: lim n→∞.x[n] = y,
cauchy: cauchy(n.x[n]),
converges: x[n]↓ as n→∞,
all: ∀x:A. B[x],
implies: P ⇒ Q,
so_lambda: λ2x.t[x],
member: t ∈ T,
so_apply: x[s],
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
uall: ∀[x:A]. B[x],
prop: ℙ
Lemmas referenced :
converges-iff-cauchy,
istype-nat,
cauchy_wf,
real_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
sqequalRule,
lambdaFormation_alt,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
lambdaEquality_alt,
applyEquality,
hypothesisEquality,
productElimination,
independent_functionElimination,
universeIsType,
isectElimination,
functionIsType
Latex:
mcomplete(\mBbbR{} with rmetric())
Date html generated:
2019_10_30-AM-06_43_51
Last ObjectModification:
2019_10_02-AM-10_56_13
Theory : reals
Home
Index