---

Step * 1 2 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])
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)
BY
{ (D -1 THEN InstLemma `common-limit-midpoints` [⌜λ2n.fst(h[n])⌝;⌜λ2n.snd(h[n])⌝]⋅ THEN Auto) }

1
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. a : ℝ
4. A[a]
5. b : ℝ
6. B[b]
7. d : r:ℝ ⟶ (A[r] + B[r])
8. h : ℕ ⟶ (ℝ × ℝ)
9. ∀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> ∈ (ℝ × ℝ))))
10. n : ℕ
⊢ (((fst(h[n + 1])) = (fst(h[n]))) ∧ ((snd(h[n + 1])) = ((fst(h[n])) + (snd(h[n]))/r(2))))
∨ (((fst(h[n + 1])) = ((fst(h[n])) + (snd(h[n]))/r(2))) ∧ ((snd(h[n + 1])) = (snd(h[n]))))

2
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. a : ℝ
4. A[a]
5. b : ℝ
6. B[b]
7. d : r:ℝ ⟶ (A[r] + B[r])
8. h : ℕ ⟶ (ℝ × ℝ)
9. ∀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> ∈ (ℝ × ℝ))))
10. ∃y:ℝ. (lim n→∞.fst(h[n]) = y ∧ lim n→∞.snd(h[n]) = y)
⊢ ∃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])
8.  \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>)))
\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  InstLemma  `common-limit-midpoints`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.fst(h[n])\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.snd(h[n])\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index