---

Step * of Lemma stream-bijection

∀[A:Type]. Bij(stream(A);ℕ ⟶ A;λs,n. s-nth(n;s))
BY
{ Auto }

1
1. [A] : Type
⊢ Bij(stream(A);ℕ ⟶ A;λs,n. s-nth(n;s))

---

Latex:

---

Latex:
\mforall{}[A:Type].  Bij(stream(A);\mBbbN{}  {}\mrightarrow{}  A;\mlambda{}s,n.  s-nth(n;s))


By

---

Latex:
Auto

---

Home Index