---

Step * of Lemma firstn_map

∀[f:Top]. ∀[n:ℕ]. ∀[l:Top List].  (firstn(n;map(f;l)) ~ map(f;firstn(n;l)))
BY
{ InductionOnNat }

1
.....basecase..... 
1. f : Top
2. n : ℤ
⊢ ∀[l:Top List]. (firstn(0;map(f;l)) ~ map(f;firstn(0;l)))

2
.....upcase..... 
1. f : Top
2. n : ℤ
3. 0 < n
4. ∀[l:Top List]. (firstn(n - 1;map(f;l)) ~ map(f;firstn(n - 1;l)))
⊢ ∀[l:Top List]. (firstn(n;map(f;l)) ~ map(f;firstn(n;l)))

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[n:\mBbbN{}].  \mforall{}[l:Top  List].    (firstn(n;map(f;l))  \msim{}  map(f;firstn(n;l)))


By

---

Latex:
InductionOnNat

---

Home Index