---

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

.....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> ∈ (ℝ × ℝ))))
BY
{ ((InstLemma `cover-seq-property-ext` [⌜A⌝;⌜B⌝;⌜d⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN D 0 With ⌜λn.cover-seq(d;a;b;n)⌝ 
   THEN All (RepUR ``so_apply``)
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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{}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>)))


By

---

Latex:
((InstLemma  `cover-seq-property-ext`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  0  With  \mkleeneopen{}\mlambda{}n.cover-seq(d;a;b;n)\mkleeneclose{} 
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto)

---

Home Index