---

Step * 2 of Lemma sp-lub-is-bottom


1. A : ℕ ⟶ Sierpinski
2. ∀n:ℕ. (A[n] = ⊥ ∈ Sierpinski)
⊢ lub(n.A[n]) = ⊥ ∈ Sierpinski
BY
{ TACTIC:((RWO "-1" 0 THENA Auto)
          THEN RepUR ``sp-lub Sierpinski-bottom`` 0
          THEN EqTypeCD
          THEN Reduce 0
          THEN Auto
          THEN (RWO "equal-Sierpinski-bottom" 0 THENA Auto)
          THEN Reduce 0
          THEN (RWW "assert-b-exists" 0 THENA Auto)
          THEN Reduce 0) }

1
1. A : ℕ ⟶ Sierpinski
2. ∀n:ℕ. (A[n] = ⊥ ∈ Sierpinski)
3. (λn.ff) = ⊥ ∈ (ℕ ⟶ 𝔹)
⊢ ∀n:ℕ. (¬↑let i,j = coded-pair(n) in ff)

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}  {}\mrightarrow{}  Sierpinski
2.  \mforall{}n:\mBbbN{}.  (A[n]  =  \mbot{})
\mvdash{}  lub(n.A[n])  =  \mbot{}


By

---

Latex:
TACTIC:((RWO  "-1"  0  THENA  Auto)
                THEN  RepUR  ``sp-lub  Sierpinski-bottom``  0
                THEN  EqTypeCD
                THEN  Reduce  0
                THEN  Auto
                THEN  (RWO  "equal-Sierpinski-bottom"  0  THENA  Auto)
                THEN  Reduce  0
                THEN  (RWW  "assert-b-exists"  0  THENA  Auto)
                THEN  Reduce  0)

---

Home Index