---

Step * 1 of Lemma select_listify_id


1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. i : ℕn
⊢ (f)[ℕn][i] = (f i) ∈ T
BY
{ (Assert ⌜∀j:{...n}. ((0 ≤ j) ⇒ (∀i:{j..n-}. (listify(f;j;n)[i - j] = (f i) ∈ T)))⌝ THENA Thin 4) }

1
1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
⊢ ∀j:{...n}. ((0 ≤ j) ⇒ (∀i:{j..n-}. (listify(f;j;n)[i - j] = (f i) ∈ T)))

2
1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. i : ℕn
5. ∀j:{...n}. ((0 ≤ j) ⇒ (∀i:{j..n-}. (listify(f;j;n)[i - j] = (f i) ∈ T)))
⊢ (f)[ℕn][i] = (f i) ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
4.  i  :  \mBbbN{}n
\mvdash{}  (f)[\mBbbN{}n][i]  =  (f  i)


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}j:\{...n\}.  ((0  \mleq{}  j)  {}\mRightarrow{}  (\mforall{}i:\{j..n\msupminus{}\}.  (listify(f;j;n)[i  -  j]  =  (f  i))))\mkleeneclose{}  THENA  Thin  4)

---

Home Index