---

Step * 1 of Lemma not-Sierpinski-top


1. (⊥ = ⊤ ∈ (ℕ ⟶ 𝔹)) ⇒ False
2. x : Base
3. x ∈ ℕ ⟶ 𝔹
4. ⊥ = ⊥ ∈ (ℕ ⟶ 𝔹)
5. n : ℕ
6. ↑(x n)
7. x = ⊥ ∈ (ℕ ⟶ 𝔹)
⊢ ⊤ = ⊥ ∈ (ℕ ⟶ 𝔹)
BY
{ TACTIC:(ApFunToHypEquands `F' ⌜F n⌝ ⌜𝔹⌝ (-1)⋅ THEN Auto THEN RepUR ``Sierpinski-bottom`` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  (\mbot{}  =  \mtop{})  {}\mRightarrow{}  False
2.  x  :  Base
3.  x  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
4.  \mbot{}  =  \mbot{}
5.  n  :  \mBbbN{}
6.  \muparrow{}(x  n)
7.  x  =  \mbot{}
\mvdash{}  \mtop{}  =  \mbot{}


By

---

Latex:
TACTIC:(ApFunToHypEquands  `F'  \mkleeneopen{}F  n\mkleeneclose{}  \mkleeneopen{}\mBbbB{}\mkleeneclose{}  (-1)\mcdot{}
                THEN  Auto
                THEN  RepUR  ``Sierpinski-bottom``  -1
                THEN  Auto)

---

Home Index