---

Step * 1 of Lemma sp-lub-is-top1


1. A : ℕ ⟶ Sierpinski
2. lub(n.A[n]) = ⊤ ∈ Sierpinski
⊢ ¬(∀n:ℕ. (A[n] = ⊥ ∈ Sierpinski))
BY
{ TACTIC:(Assert ¬(lub(n.A[n]) = ⊥ ∈ Sierpinski) BY
                (D 0 THEN Auto THEN InstLemma `Sierpinski-unequal`[] THEN Auto)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(Assert  \mneg{}(lub(n.A[n])  =  \mbot{})  BY
                            (D  0  THEN  Auto  THEN  InstLemma  `Sierpinski-unequal`[]  THEN  Auto))

---

Home Index