---

Step * of Lemma inhabited-covers-reals-implies

∀[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
{ (Assert ∃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))))))))) BY
         (D 0 With ⌜(r1/r(2))⌝  THEN Auto)) }

1
1. r0 ≤ (r1/r(2))
2. (r1/r(2)) < r1
3. [A] : ℝ ⟶ ℙ
4. [B] : ℝ ⟶ ℙ
5. ∀r:ℝ. (A[r] ∨ B[r])
6. a : ℝ
7. b : ℝ
8. A a
9. B b
10. a ≤ b
⊢ ∃a',b':ℝ. ((A a') ∧ (B b') ∧ (a ≤ a') ∧ (a' ≤ b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * (r1/r(2)))))

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)))))))))
⊢ ∀[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)))

---

Latex:

---

Latex:
\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:
(Assert  \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)))))))))  BY
              (D  0  With  \mkleeneopen{}(r1/r(2))\mkleeneclose{}    THEN  Auto))

---

Home Index