---

Step * of Lemma sp-lub-is-bottom

∀[A:ℕ ⟶ Sierpinski]. (lub(n.A[n]) = ⊥ ∈ Sierpinski ⇐⇒ ∀n:ℕ. (A[n] = ⊥ ∈ Sierpinski))
BY
{ Auto }

1
1. A : ℕ ⟶ Sierpinski
2. lub(n.A[n]) = ⊥ ∈ Sierpinski
3. n : ℕ
⊢ A[n] = ⊥ ∈ Sierpinski

2
1. A : ℕ ⟶ Sierpinski
2. ∀n:ℕ. (A[n] = ⊥ ∈ Sierpinski)
⊢ lub(n.A[n]) = ⊥ ∈ Sierpinski

---

Latex:

---

Latex:
\mforall{}[A:\mBbbN{}  {}\mrightarrow{}  Sierpinski].  (lub(n.A[n])  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}.  (A[n]  =  \mbot{}))


By

---

Latex:
Auto

---

Home Index