Step
*
of Lemma
equipollent-product-zero
∀[A:Type]. (A × ℕ0 ~ ℕ0 ∧ ℕ0 × A ~ ℕ0)
BY
{ Auto }
1
1. [A] : Type
⊢ A × ℕ0 ~ ℕ0
2
1. [A] : Type
2. A × ℕ0 ~ ℕ0
⊢ ℕ0 × A ~ ℕ0
Latex:
Latex:
\mforall{}[A:Type]. (A \mtimes{} \mBbbN{}0 \msim{} \mBbbN{}0 \mwedge{} \mBbbN{}0 \mtimes{} A \msim{} \mBbbN{}0)
By
Latex:
Auto
Home
Index