---

Step * 2 2 2 of Lemma inhabited-covers-reals-implies


1. ∃c:ℝ
    (((r0 ≤ c) ∧ (c < r1))
    ∧ (∀[A,B:ℝ ⟶ ℙ].
         ((∀r:ℝ. (A[r] ∨ B[r]))
         ⇒ (∀a,b:ℝ.
               (((A a) ∧ (B b) ∧ (a ≤ b))
               ⇒ (∃a',b':ℝ. ((A a') ∧ (B b') ∧ (a ≤ a') ∧ (a' ≤ b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))))))))
2. [A] : ℝ ⟶ ℙ
3. [B] : ℝ ⟶ ℙ
4. ∃a:ℝ. A[a]
5. ∃b:ℝ. B[b]
6. ∀r:ℝ. (A[r] ∨ B[r])
7. a : ℝ
8. b : ℝ
9. A a
10. B b
11. a ≤ b
12. ∃y:ℝ. (y ∈ closure(A) ∧ y ∈ closure(B))
⊢ ∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)
BY
{ ((D -1 THEN RenameVar `x' (-2) THEN D -1)
   THEN (D -2 THEN RenameVar `f' (-3))
   THEN (D -1 THEN RenameVar `g' (-2))
   THEN InstConcl [⌜f⌝;⌜g⌝;⌜x⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  \mexists{}c:\mBbbR{}
        (((r0  \mleq{}  c)  \mwedge{}  (c  <  r1))
        \mwedge{}  (\mforall{}[A,B:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
                  ((\mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r]))
                  {}\mRightarrow{}  (\mforall{}a,b:\mBbbR{}.
                              (((A  a)  \mwedge{}  (B  b)  \mwedge{}  (a  \mleq{}  b))
                              {}\mRightarrow{}  (\mexists{}a',b':\mBbbR{}
                                        ((A  a')
                                        \mwedge{}  (B  b')
                                        \mwedge{}  (a  \mleq{}  a')
                                        \mwedge{}  (a'  \mleq{}  b')
                                        \mwedge{}  (b'  \mleq{}  b)
                                        \mwedge{}  ((b'  -  a')  \mleq{}  ((b  -  a)  *  c)))))))))
2.  [A]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  [B]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
4.  \mexists{}a:\mBbbR{}.  A[a]
5.  \mexists{}b:\mBbbR{}.  B[b]
6.  \mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r])
7.  a  :  \mBbbR{}
8.  b  :  \mBbbR{}
9.  A  a
10.  B  b
11.  a  \mleq{}  b
12.  \mexists{}y:\mBbbR{}.  (y  \mmember{}  closure(A)  \mwedge{}  y  \mmember{}  closure(B))
\mvdash{}  \mexists{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mexists{}x:\mBbbR{}.  ((\mforall{}n:\mBbbN{}.  A[f  n])  \mwedge{}  (\mforall{}n:\mBbbN{}.  B[g  n])  \mwedge{}  lim  n\mrightarrow{}\minfty{}.f  n  =  x  \mwedge{}  lim  n\mrightarrow{}\minfty{}.g  n  =  x)


By

---

Latex:
((D  -1  THEN  RenameVar  `x'  (-2)  THEN  D  -1)
  THEN  (D  -2  THEN  RenameVar  `f'  (-3))
  THEN  (D  -1  THEN  RenameVar  `g'  (-2))
  THEN  InstConcl  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index