---

Step * 2 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)
⊢ ↓∃L@0:T2 List. ((L@0 = map(f;L) ∈ bag(T2)) ∧ no_repeats(T2;L@0))
BY
{ D 0 }

1
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)
⊢ ∃L@0:T2 List. ((L@0 = map(f;L) ∈ bag(T2)) ∧ no_repeats(T2;L@0))

---

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
\mvdash{}  \mdownarrow{}\mexists{}L@0:T2  List.  ((L@0  =  map(f;L))  \mwedge{}  no\_repeats(T2;L@0))


By

---

Latex:
D  0

---

Home Index