---

Step * 1 of Lemma member_map


1. [T] : Type
2. [T'] : Type
3. a : T List
4. x : T'
5. f : T ⟶ T'
6. ∃i:ℕ. (i < ||map(f;a)|| c∧ (x = map(f;a)[i] ∈ T'))
⊢ ∃y:T. ((∃i:ℕ. (i < ||a|| c∧ (y = a[i] ∈ T))) ∧ (x = (f y) ∈ T'))
BY
{ ((((ExRepD THEN RWW "map_length" (-2)) THENA Auto) THEN RWW "map_select" (-1)) THENA Auto) }

1
1. [T] : Type
2. [T'] : Type
3. a : T List
4. x : T'
5. f : T ⟶ T'
6. i : ℕ
7. i < ||a||
8. x = (f a[i]) ∈ T'
⊢ ∃y:T. ((∃i:ℕ. (i < ||a|| c∧ (y = a[i] ∈ T))) ∧ (x = (f y) ∈ T'))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [T']  :  Type
3.  a  :  T  List
4.  x  :  T'
5.  f  :  T  {}\mrightarrow{}  T'
6.  \mexists{}i:\mBbbN{}.  (i  <  ||map(f;a)||  c\mwedge{}  (x  =  map(f;a)[i]))
\mvdash{}  \mexists{}y:T.  ((\mexists{}i:\mBbbN{}.  (i  <  ||a||  c\mwedge{}  (y  =  a[i])))  \mwedge{}  (x  =  (f  y)))


By

---

Latex:
((((ExRepD  THEN  RWW  "map\_length"  (-2))  THENA  Auto)  THEN  RWW  "map\_select"  (-1))  THENA  Auto)

---

Home Index