---

Step * 1 of Lemma stream-bijection


1. [A] : Type
⊢ Bij(stream(A);ℕ ⟶ A;λs,n. s-nth(n;s))
BY
{ (RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto) }

1
1. A : Type
2. a1 : stream(A)
3. a2 : stream(A)
4. (λn.s-nth(n;a1)) = (λn.s-nth(n;a2)) ∈ (ℕ ⟶ A)
⊢ a1 = a2 ∈ stream(A)

2
1. [A] : Type
2. b : ℕ ⟶ A
⊢ ∃a:stream(A). ((λn.s-nth(n;a)) = b ∈ (ℕ ⟶ A))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Auto)

---

Home Index