---

Step * 2 of Lemma mklist_select

.....upcase..... 
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀[f:ℕn - 1 ⟶ T]. ∀[i:ℕn - 1].  (mklist(n - 1;f)[i] = (f i) ∈ T)
⊢ ∀[f:ℕn ⟶ T]. ∀[i:ℕn].  (mklist(n;f)[i] = (f i) ∈ T)
BY
{ (ParallelOp (-1)) }

1
1. T : Type
2. n : ℤ
3. 0 < n
4. ∀[f:ℕn - 1 ⟶ T]. ∀[i:ℕn - 1].  (mklist(n - 1;f)[i] = (f i) ∈ T)
5. [f] : ℕn ⟶ T
6. ∀[i:ℕn - 1]. (mklist(n - 1;f)[i] = (f i) ∈ T)
⊢ ∀[i:ℕn]. (mklist(n;f)[i] = (f i) ∈ T)

---

Latex:

---

Latex:
.....upcase..... 
1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  T].  \mforall{}[i:\mBbbN{}n  -  1].    (mklist(n  -  1;f)[i]  =  (f  i))
\mvdash{}  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  T].  \mforall{}[i:\mBbbN{}n].    (mklist(n;f)[i]  =  (f  i))


By

---

Latex:
(ParallelOp  (-1))

---

Home Index