---

Step * 2 of Lemma fun2listCantor


1. n : ℤ
2. [%1] : 0 < n
3. ∀f:ℕn - 1 ⟶ 𝔹. ∃l:𝔹 List. ((||l|| = (n - 1) ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn - 1 ⟶ 𝔹)))
4. f : ℕn ⟶ 𝔹
⊢ ∃l:𝔹 List. ((||l|| = n ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn ⟶ 𝔹)))
BY
{ TACTIC:((InstHyp [⌜f⌝] (-2)⋅ THENA Auto) THEN ExRepD) }

1
1. n : ℤ
2. [%1] : 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 ⟶ 𝔹)
⊢ ∃l:𝔹 List. ((||l|| = n ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn ⟶ 𝔹)))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  [\%1]  :  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{}
\mvdash{}  \mexists{}l:\mBbbB{}  List.  ((||l||  =  n)  \mwedge{}  (f  =  (\mlambda{}x.l[x])))


By

---

Latex:
TACTIC:((InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index