---

Step * 2 of Lemma fun-converges-iff-cauchy


1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. λn.f[n;x] is cauchy for x ∈ I
⊢ λn.f[n;x]↓ for x ∈ I)
BY
{ (Assert ∀x:{x:ℝ| x ∈ I} . f[n;x]↓ as n→∞ BY
         (Auto
          THEN BLemma `converges-iff-cauchy`
          THEN Auto
          THEN (InstLemma `i-member-witness` [⌜I⌝;⌜x⌝]⋅ THENA Auto)
          THEN D -1
          THEN (With ⌜n⌝ (D 3)⋅
                THENA (Auto THEN MemTypeCD THEN Auto THEN (D 0 THEN Auto) THEN With ⌜x⌝ (D 0)⋅ THEN Auto)
                )
          THEN Unfold `cauchy` 0
          THEN ParallelLast
          THEN D -1
          THEN With ⌜N⌝ (D 0)⋅
          THEN Auto)) }

1
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. λn.f[n;x] is cauchy for x ∈ I
4. ∀x:{x:ℝ| x ∈ I} . f[n;x]↓ as n→∞
⊢ λn.f[n;x]↓ for x ∈ I)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  \mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}
3.  \mlambda{}n.f[n;x]  is  cauchy  for  x  \mmember{}  I
\mvdash{}  \mlambda{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  I)


By

---

Latex:
(Assert  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  f[n;x]\mdownarrow{}  as  n\mrightarrow{}\minfty{}  BY
              (Auto
                THEN  BLemma  `converges-iff-cauchy`
                THEN  Auto
                THEN  (InstLemma  `i-member-witness`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  D  -1
                THEN  (With  \mkleeneopen{}n\mkleeneclose{}  (D  3)\mcdot{}
                            THENA  (Auto
                                          THEN  MemTypeCD
                                          THEN  Auto
                                          THEN  (D  0  THEN  Auto)
                                          THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}
                                          THEN  Auto)
                            )
                THEN  Unfold  `cauchy`  0
                THEN  ParallelLast
                THEN  D  -1
                THEN  With  \mkleeneopen{}N\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto))

---

Home Index