---

Step * 2 1 1 of Lemma bag-map-no-repeats


1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ T2
4. bs : T1 List
5. Inj(T1;T2;f)
6. L : T1 List
7. no_repeats(T1;L)
8. L = bs ∈ bag(T1)
9. bag-map(f;L) = bag-map(f;L) ∈ bag(T2)
⊢ Inj({x:T1| (x ∈ L)} ;T2;f)
BY
{ (RepeatFor 2 (ParallelOp 5) THEN RepeatFor 2 (ParallelLast) THEN All DSet THEN EqTypeCD THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  f  :  T1  {}\mrightarrow{}  T2
4.  bs  :  T1  List
5.  Inj(T1;T2;f)
6.  L  :  T1  List
7.  no\_repeats(T1;L)
8.  L  =  bs
9.  bag-map(f;L)  =  bag-map(f;L)
\mvdash{}  Inj(\{x:T1|  (x  \mmember{}  L)\}  ;T2;f)


By

---

Latex:
(RepeatFor  2  (ParallelOp  5)  THEN  RepeatFor  2  (ParallelLast)  THEN  All  DSet  THEN  EqTypeCD  THEN  Auto)\mcdot{}

---

Home Index