---

Step * of Lemma sp-lub-is-top

∀[A:ℕ ⟶ Sierpinski]. (lub(n.A[n]) = ⊤ ∈ Sierpinski ⇐⇒ ¬¬(∃n:ℕ. (A[n] = ⊤ ∈ Sierpinski)))
BY
{ ((D 0 THENA Auto) THEN RWO "sp-lub-is-top1" 0 THEN Auto) }

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

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

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)  THEN  RWO  "sp-lub-is-top1"  0  THEN  Auto)

---

Home Index