---

Step * 1 2 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 : ℕ ⟶ (ℝ × ℝ)
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)
BY
{ (ExRepD THEN InstConcl [⌜λn.(fst(h[n]))⌝;⌜λn.(snd(h[n]))⌝;⌜y⌝]⋅ THEN Auto THEN Reduce 0 THEN Auto) }

---

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.  h  :  \mBbbN{}  {}\mrightarrow{}  (\mBbbR{}  \mtimes{}  \mBbbR{})
9.  \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>)))
10.  \mexists{}y:\mBbbR{}.  (lim  n\mrightarrow{}\minfty{}.fst(h[n])  =  y  \mwedge{}  lim  n\mrightarrow{}\minfty{}.snd(h[n])  =  y)
\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:
(ExRepD  THEN  InstConcl  [\mkleeneopen{}\mlambda{}n.(fst(h[n]))\mkleeneclose{};\mkleeneopen{}\mlambda{}n.(snd(h[n]))\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Reduce  0  THEN  Auto)

---

Home Index