---

Step * 1 of Lemma inhabited-covers-real-implies


1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. a : ℝ
4. A[a]
5. b : ℝ
6. B[b]
7. d : 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 ⌜∃h:ℕ ⟶ (ℝ × ℝ)
           ∀n:ℕ
             (A[fst(h[n])]
             ∧ B[snd(h[n])]
             ∧ ((h[n + 1] = let a,b = h[n] in <a, (a + b/r(2))> ∈ (ℝ × ℝ))
               ∨ (h[n + 1] = let a,b = h[n] in <(a + b/r(2)), b> ∈ (ℝ × ℝ))))⌝⋅ }

1
.....assertion..... 
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. a : ℝ
4. A[a]
5. b : ℝ
6. B[b]
7. d : r:ℝ ⟶ (A[r] + B[r])
⊢ ∃h:ℕ ⟶ (ℝ × ℝ)
   ∀n:ℕ
     (A[fst(h[n])]
     ∧ B[snd(h[n])]
     ∧ ((h[n + 1] = let a,b = h[n] in <a, (a + b/r(2))> ∈ (ℝ × ℝ))
       ∨ (h[n + 1] = let a,b = h[n] in <(a + b/r(2)), b> ∈ (ℝ × ℝ))))

2
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. a : ℝ
4. A[a]
5. b : ℝ
6. B[b]
7. d : r:ℝ ⟶ (A[r] + B[r])
8. ∃h:ℕ ⟶ (ℝ × ℝ)
    ∀n:ℕ
      (A[fst(h[n])]
      ∧ B[snd(h[n])]
      ∧ ((h[n + 1] = let a,b = h[n] in <a, (a + b/r(2))> ∈ (ℝ × ℝ))
        ∨ (h[n + 1] = let a,b = h[n] in <(a + b/r(2)), b> ∈ (ℝ × ℝ))))
⊢ ∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)

---

Latex:

---

Latex:

1.  [A]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  [B]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  a  :  \mBbbR{}
4.  A[a]
5.  b  :  \mBbbR{}
6.  B[b]
7.  d  :  r:\mBbbR{}  {}\mrightarrow{}  (A[r]  +  B[r])
\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:
Assert  \mkleeneopen{}\mexists{}h:\mBbbN{}  {}\mrightarrow{}  (\mBbbR{}  \mtimes{}  \mBbbR{})
                  \mforall{}n:\mBbbN{}
                      (A[fst(h[n])]
                      \mwedge{}  B[snd(h[n])]
                      \mwedge{}  ((h[n  +  1]  =  let  a,b  =  h[n]  in  <a,  (a  +  b/r(2))>)
                          \mvee{}  (h[n  +  1]  =  let  a,b  =  h[n]  in  <(a  +  b/r(2)),  b>)))\mkleeneclose{}\mcdot{}

---

Home Index