---

Step * 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)))))))))
⊢ ∀[A,B:ℝ ⟶ ℙ].
    ((∃a:ℝ. A[a])
    ⇒ (∃b:ℝ. B[b])
    ⇒ (∀r:ℝ. (A[r] ∨ B[r]))
    ⇒ (∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)))
BY
{ (Auto THEN Assert ⌜∃a,b:ℝ. ((A a) ∧ (B b) ∧ ((a ≤ b) ∨ (b ≤ a)))⌝⋅) }

1
.....assertion..... 
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])
⊢ ∃a,b:ℝ. ((A a) ∧ (B b) ∧ ((a ≤ b) ∨ (b ≤ a)))

2
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,b:ℝ. ((A a) ∧ (B b) ∧ ((a ≤ b) ∨ (b ≤ a)))
⊢ ∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)

---

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)))))))))
\mvdash{}  \mforall{}[A,B:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
        ((\mexists{}a:\mBbbR{}.  A[a])
        {}\mRightarrow{}  (\mexists{}b:\mBbbR{}.  B[b])
        {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r]))
        {}\mRightarrow{}  (\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:
(Auto  THEN  Assert  \mkleeneopen{}\mexists{}a,b:\mBbbR{}.  ((A  a)  \mwedge{}  (B  b)  \mwedge{}  ((a  \mleq{}  b)  \mvee{}  (b  \mleq{}  a)))\mkleeneclose{}\mcdot{})

---

Home Index