Step * of Lemma equipollent-product-one

[A:Type]. (A × ℕA ∧ ℕ1 × A)
BY
TACTIC:Assert ⌜ℕTop⌝⋅ }

1
.....assertion..... 
Top

2
1. ℕTop
⊢ ∀[A:Type]. (A × ℕA ∧ ℕ1 × A)


Latex:


Latex:
\mforall{}[A:Type].  (A  \mtimes{}  \mBbbN{}1  \msim{}  A  \mwedge{}  \mBbbN{}1  \mtimes{}  A  \msim{}  A)


By


Latex:
TACTIC:Assert  \mkleeneopen{}\mBbbN{}1  \msim{}  Top\mkleeneclose{}\mcdot{}




Home Index