Nuprl Lemma : reals-complete-ext
mcomplete(ℝ with rmetric())
Proof
Definitions occuring in Statement :
mcomplete: mcomplete(M),
mk-metric-space: X with d,
rmetric: rmetric(),
real: ℝ
Definitions unfolded in proof :
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
accelerate: accelerate(k;f),
reals-complete,
converges-iff-cauchy
Latex:
mcomplete(\mBbbR{} with rmetric())
Date html generated:
2020_05_20-AM-11_56_51
Last ObjectModification:
2020_03_19-PM-04_34_01
Theory : reals
Home
Index