---

Step * of Lemma fun2listCantor

∀n:ℕ. ∀f:ℕn ⟶ 𝔹.  ∃l:𝔹 List. ((||l|| = n ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn ⟶ 𝔹)))
BY
{ TACTIC:((D 0 THENA Auto) THEN (NatInd (-1) THENA Auto) THEN (UnivCD THENA Auto)) }

1
1. f : ℕ0 ⟶ 𝔹
⊢ ∃l:𝔹 List. ((||l|| = 0 ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕ0 ⟶ 𝔹)))

2
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 ⟶ 𝔹)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    \mexists{}l:\mBbbB{}  List.  ((||l||  =  n)  \mwedge{}  (f  =  (\mlambda{}x.l[x])))


By

---

Latex:
TACTIC:((D  0  THENA  Auto)  THEN  (NatInd  (-1)  THENA  Auto)  THEN  (UnivCD  THENA  Auto))

---

Home Index