---

Step * of Lemma real-interval-complete

∀a,b:ℝ.  mcomplete({x:ℝ| x ∈ [a, b]}  with rmetric())
BY
{ (Auto
   THEN InstLemma `converges-iff-cauchy` []
   THEN RepUR ``mcomplete mcauchy mconverges mconverges-to mdist rmetric`` 0
   THEN Auto
   THEN Fold `cauchy` (-1)
   THEN Fold `converges-to` 0
   THEN (Assert x[n]↓ as n→∞ BY
               Auto)
   THEN (D -1 THEN D 0 With ⌜y⌝ )
   THEN Auto
   THEN MemTypeCD
   THEN Auto) }

1
1. a : ℝ
2. b : ℝ
3. ∀x:ℕ ⟶ ℝ. (x[n]↓ as n→∞ ⇐⇒ cauchy(n.x[n]))
4. x : ℕ ⟶ {x:ℝ| (a ≤ x) ∧ (x ≤ b)} 
5. cauchy(n.x n)
6. y : ℝ
7. lim n→∞.x[n] = y
⊢ a ≤ y

2
1. a : ℝ
2. b : ℝ
3. ∀x:ℕ ⟶ ℝ. (x[n]↓ as n→∞ ⇐⇒ cauchy(n.x[n]))
4. x : ℕ ⟶ {x:ℝ| (a ≤ x) ∧ (x ≤ b)} 
5. cauchy(n.x n)
6. y : ℝ
7. lim n→∞.x[n] = y
8. a ≤ y
⊢ y ≤ b

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    mcomplete(\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}    with  rmetric())


By

---

Latex:
(Auto
  THEN  InstLemma  `converges-iff-cauchy`  []
  THEN  RepUR  ``mcomplete  mcauchy  mconverges  mconverges-to  mdist  rmetric``  0
  THEN  Auto
  THEN  Fold  `cauchy`  (-1)
  THEN  Fold  `converges-to`  0
  THEN  (Assert  x[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{}  BY
                          Auto)
  THEN  (D  -1  THEN  D  0  With  \mkleeneopen{}y\mkleeneclose{}  )
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index