---

Step * of Lemma equipollent-powerset

∀n:ℕ. ∀T:Type.  (T ~ ℕn ⇒ powerset(T) ~ ℕ2^n)
BY
{ ((Auto THEN Unfold `powerset` 0) THEN RWO "-1" 0 THEN Auto THEN BLemma `equipollent-exp` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}T:Type.    (T  \msim{}  \mBbbN{}n  {}\mRightarrow{}  powerset(T)  \msim{}  \mBbbN{}2\^{}n)


By

---

Latex:
((Auto  THEN  Unfold  `powerset`  0)  THEN  RWO  "-1"  0  THEN  Auto  THEN  BLemma  `equipollent-exp`  THEN  Auto)

---

Home Index