---

Step * 2 1 1 1 of Lemma mklist_select


1. T : Type
2. n : ℤ
3. ¬n < 1
4. 0 < n
5. ∀[f:ℕn - 1 ⟶ T]. ∀[i:ℕn - 1].  (mklist(n - 1;f)[i] = (f i) ∈ T)
6. f : ℕn ⟶ T
7. ∀[i:ℕn - 1]. (mklist(n - 1;f)[i] = (f i) ∈ T)
8. i : ℕn
⊢ mklist(n - 1;f) @ [f (n - 1)][i] = (f i) ∈ T
BY
{ (Decide i < n - 1 THENA Auto) }

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

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbZ{}
3.  \mneg{}n  <  1
4.  0  <  n
5.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  T].  \mforall{}[i:\mBbbN{}n  -  1].    (mklist(n  -  1;f)[i]  =  (f  i))
6.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
7.  \mforall{}[i:\mBbbN{}n  -  1].  (mklist(n  -  1;f)[i]  =  (f  i))
8.  i  :  \mBbbN{}n
\mvdash{}  mklist(n  -  1;f)  @  [f  (n  -  1)][i]  =  (f  i)


By

---

Latex:
(Decide  i  <  n  -  1  THENA  Auto)

---

Home Index