---

Step * 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 : T2 List
7. L = map(f;bs) ∈ bag(T2)
8. no_repeats(T2;L)
⊢ ↓∃L:T1 List. ((L = bs ∈ bag(T1)) ∧ no_repeats(T1;L))
BY
{ ((EqTypeHD (-2) THEN Auto)
   THEN D 0
   THEN With ⌜bs⌝ (D 0)⋅
   THEN Auto
   THEN FLemma `no_repeats_functionality_wrt_permutation` [-3;-2]
   THEN Auto
   THEN RepeatFor 7 ((ParallelLast' THENA (RWO "length-map" 0 THEN Auto)))) }

1
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ T2
4. bs : T1 List
5. Inj(T1;T2;f)
6. L : T2 List
7. L = map(f;bs) ∈ pertype(λas,bs. ((as ∈ T2 List) ∧ (bs ∈ T2 List) ∧ permutation(T2;as;bs)))
8. L ∈ T2 List
9. map(f;bs) ∈ T2 List
10. permutation(T2;L;map(f;bs))
11. no_repeats(T2;L)
12. bs = bs ∈ bag(T1)
13. i : ℕ
14. j : ℕ
15. i < ||bs||
16. j < ||bs||
17. ¬(i = j ∈ ℕ)
18. bs[i] = bs[j] ∈ T1
⊢ map(f;bs)[i] = map(f;bs)[j] ∈ T2

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  f  :  T1  {}\mrightarrow{}  T2
4.  bs  :  T1  List
5.  Inj(T1;T2;f)
6.  L  :  T2  List
7.  L  =  map(f;bs)
8.  no\_repeats(T2;L)
\mvdash{}  \mdownarrow{}\mexists{}L:T1  List.  ((L  =  bs)  \mwedge{}  no\_repeats(T1;L))


By

---

Latex:
((EqTypeHD  (-2)  THEN  Auto)
  THEN  D  0
  THEN  With  \mkleeneopen{}bs\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  FLemma  `no\_repeats\_functionality\_wrt\_permutation`  [-3;-2]
  THEN  Auto
  THEN  RepeatFor  7  ((ParallelLast'  THENA  (RWO  "length-map"  0  THEN  Auto))))

---

Home Index