---

Step * of Lemma sp-lub-is-top1

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

1
1. A : ℕ ⟶ Sierpinski
2. lub(n.A[n]) = ⊤ ∈ Sierpinski
⊢ ¬(∀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])  =  \mtop{}  \mLeftarrow{}{}\mRightarrow{}  \mneg{}(\mforall{}n:\mBbbN{}.  (A[n]  =  \mbot{})))


By

---

Latex:
TACTIC:Auto

---

Home Index