---

Step * 1 1 of Lemma bag-member-map


1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. L : T List
⊢ x ↓∈ bag-map(f;L) ⇒ (↓∃v:T. (v ↓∈ L ∧ (x = (f v) ∈ U)))
BY
{ ListInd (-1) }

1
1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
⊢ x ↓∈ bag-map(f;[]) ⇒ (↓∃v:T. (v ↓∈ [] ∧ (x = (f v) ∈ U)))

2
1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. u : T
6. v : T List
7. x ↓∈ bag-map(f;v) ⇒ (↓∃v@0:T. (v@0 ↓∈ v ∧ (x = (f v@0) ∈ U)))
⊢ x ↓∈ bag-map(f;[u / v]) ⇒ (↓∃v@0:T. (v@0 ↓∈ [u / v] ∧ (x = (f v@0) ∈ U)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  U  :  Type
3.  x  :  U
4.  f  :  T  {}\mrightarrow{}  U
5.  L  :  T  List
\mvdash{}  x  \mdownarrow{}\mmember{}  bag-map(f;L)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  L  \mwedge{}  (x  =  (f  v))))


By

---

Latex:
ListInd  (-1)

---

Home Index