---

Step * of Lemma dense-in-interval-implies

∀I:Interval
  ∀[X:{a:ℝ| a ∈ I}  ⟶ ℙ]
    (dense-in-interval(I;X)
    ⇒ (∃u,v:{a:ℝ| a ∈ I} . u ≠ v)
    ⇒ (∀a:{a:ℝ| a ∈ I} . ∃x:ℕ ⟶ {a:ℝ| a ∈ I} . ((∀n:ℕ. (X (x n))) ∧ lim n→∞.x n = a)))
BY
{ (Auto
   THEN (Assert ∃b:{a:ℝ| a ∈ I} . b ≠ a BY
               (ExRepD THEN (InstLemma `rneq-cases` [⌜u⌝;⌜v⌝;⌜a⌝]⋅ THENM D -1) THEN Auto))
   THEN Thin (-3)
   THEN (Assert ∃b:{b:ℝ| b ∈ I} . ((X b) ∧ b ≠ a) BY
               (RepeatFor 2 (D -1)
                THEN UnfoldTopAb 3
                THEN FHyp 3 [-1]
                THEN Auto
                THEN ParallelLast
                THEN Auto
                THEN ((InstLemma `i-member-between` [⌜I⌝;⌜b⌝;⌜a⌝;⌜x⌝]⋅ THEN Complete (Auto))
                ORELSE (InstLemma `i-member-between` [⌜I⌝;⌜a⌝;⌜b⌝;⌜x⌝]⋅ THEN Complete (Auto))
                )))
   THEN Thin (-2)
   THEN Assert ⌜∀b:{b:ℝ| (b ∈ I) ∧ b ≠ a} . ∃c:{c:ℝ| (c ∈ I) ∧ c ≠ a} . ((X c) ∧ (|c - a| ≤ ((r1/r(2)) * |b - a|)))⌝⋅) }

1
.....assertion..... 
1. I : Interval
2. [X] : {a:ℝ| a ∈ I}  ⟶ ℙ
3. dense-in-interval(I;X)
4. a : {a:ℝ| a ∈ I} 
5. ∃b:{b:ℝ| b ∈ I} . ((X b) ∧ b ≠ a)
⊢ ∀b:{b:ℝ| (b ∈ I) ∧ b ≠ a} . ∃c:{c:ℝ| (c ∈ I) ∧ c ≠ a} . ((X c) ∧ (|c - a| ≤ ((r1/r(2)) * |b - a|)))

2
1. I : Interval
2. [X] : {a:ℝ| a ∈ I}  ⟶ ℙ
3. dense-in-interval(I;X)
4. a : {a:ℝ| a ∈ I} 
5. ∃b:{b:ℝ| b ∈ I} . ((X b) ∧ b ≠ a)
6. ∀b:{b:ℝ| (b ∈ I) ∧ b ≠ a} . ∃c:{c:ℝ| (c ∈ I) ∧ c ≠ a} . ((X c) ∧ (|c - a| ≤ ((r1/r(2)) * |b - a|)))
⊢ ∃x:ℕ ⟶ {a:ℝ| a ∈ I} . ((∀n:ℕ. (X (x n))) ∧ lim n→∞.x n = a)

---

Latex:

---

Latex:
\mforall{}I:Interval
    \mforall{}[X:\{a:\mBbbR{}|  a  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}]
        (dense-in-interval(I;X)
        {}\mRightarrow{}  (\mexists{}u,v:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  u  \mneq{}  v)
        {}\mRightarrow{}  (\mforall{}a:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  \mexists{}x:\mBbbN{}  {}\mrightarrow{}  \{a:\mBbbR{}|  a  \mmember{}  I\}  .  ((\mforall{}n:\mBbbN{}.  (X  (x  n)))  \mwedge{}  lim  n\mrightarrow{}\minfty{}.x  n  =  a)))


By

---

Latex:
(Auto
  THEN  (Assert  \mexists{}b:\{a:\mBbbR{}|  a  \mmember{}  I\}  .  b  \mneq{}  a  BY
                          (ExRepD  THEN  (InstLemma  `rneq-cases`  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENM  D  -1)  THEN  Auto))
  THEN  Thin  (-3)
  THEN  (Assert  \mexists{}b:\{b:\mBbbR{}|  b  \mmember{}  I\}  .  ((X  b)  \mwedge{}  b  \mneq{}  a)  BY
                          (RepeatFor  2  (D  -1)
                            THEN  UnfoldTopAb  3
                            THEN  FHyp  3  [-1]
                            THEN  Auto
                            THEN  ParallelLast
                            THEN  Auto
                            THEN  ((InstLemma  `i-member-between`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto))
                            ORELSE  (InstLemma  `i-member-between`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto))
                            )))
  THEN  Thin  (-2)
  THEN  Assert  \mkleeneopen{}\mforall{}b:\{b:\mBbbR{}|  (b  \mmember{}  I)  \mwedge{}  b  \mneq{}  a\} 
                                \mexists{}c:\{c:\mBbbR{}|  (c  \mmember{}  I)  \mwedge{}  c  \mneq{}  a\}  .  ((X  c)  \mwedge{}  (|c  -  a|  \mleq{}  ((r1/r(2))  *  |b  -  a|)))\mkleeneclose{}\mcdot{})

---

Home Index