---

Step * 1 2 of Lemma stream-bijection


1. [A] : Type
2. b : ℕ ⟶ A
⊢ ∃a:stream(A). ((λn.s-nth(n;a)) = b ∈ (ℕ ⟶ A))
BY
{ (With ⌜stream-map(b;nats())⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  b  :  \mBbbN{}  {}\mrightarrow{}  A
\mvdash{}  \mexists{}a:stream(A).  ((\mlambda{}n.s-nth(n;a))  =  b)


By

---

Latex:
(With  \mkleeneopen{}stream-map(b;nats())\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index