---

Step * of Lemma Sierpinski-unequal-1

⊥ = ⊤ ∈ (ℕ ⟶ 𝔹) ⇐⇒ False
BY
{ TACTIC:(Auto
          THEN ApFunToHypEquands `F' ⌜F 0⌝ ⌜𝔹⌝ (-1)⋅
          THEN Auto
          THEN RepUR ``Sierpinski-top Sierpinski-bottom`` -1
          THEN Auto) }

---

Latex:

---

Latex:
\mbot{}  =  \mtop{}  \mLeftarrow{}{}\mRightarrow{}  False


By

---

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

---

Home Index