---

Step * 2 1 1 1 1 of Lemma fun2listCantor


1. n : ℤ
2. 0 < n
3. ∀f:ℕn - 1 ⟶ 𝔹. ∃l:𝔹 List. ((||l|| = (n - 1) ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)))
4. f : ℕn ⟶ 𝔹
5. l : 𝔹 List
6. ||l|| = (n - 1) ∈ ℤ
7. f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)
⊢ f = (λx.l @ [f (n - 1)][x]) ∈ (ℕn ⟶ 𝔹)
BY
{ TACTIC:((FunExt THENA Auto) THEN Reduce 0) }

1
1. n : ℤ
2. 0 < n
3. ∀f:ℕn - 1 ⟶ 𝔹. ∃l:𝔹 List. ((||l|| = (n - 1) ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)))
4. f : ℕn ⟶ 𝔹
5. l : 𝔹 List
6. ||l|| = (n - 1) ∈ ℤ
7. f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)
8. x : ℕn
⊢ f x = l @ [f (n - 1)][x]

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}f:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbB{}.  \mexists{}l:\mBbbB{}  List.  ((||l||  =  (n  -  1))  \mwedge{}  (f  =  (\mlambda{}x.l[x])))
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
5.  l  :  \mBbbB{}  List
6.  ||l||  =  (n  -  1)
7.  f  =  (\mlambda{}x.l[x])
\mvdash{}  f  =  (\mlambda{}x.l  @  [f  (n  -  1)][x])


By

---

Latex:
TACTIC:((FunExt  THENA  Auto)  THEN  Reduce  0)

---

Home Index