---

Step * of Lemma bag-map-no-repeats

∀[T1,T2:Type]. ∀[f:T1 ⟶ T2]. ∀[bs:bag(T1)].
  uiff(bag-no-repeats(T2;bag-map(f;bs));bag-no-repeats(T1;bs)) supposing Inj(T1;T2;f)
BY
{ (Unfold `bag-no-repeats` 0
   THEN Auto
   THEN Unhide
   THEN Auto
   THEN SquashExRepD
   THEN (BagToList 4 THEN Auto)
   THEN All (Unfold `bag-map`)) }

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) ∈ bag(T2)
8. no_repeats(T2;L)
⊢ ↓∃L:T1 List. ((L = bs ∈ bag(T1)) ∧ no_repeats(T1;L))

2
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:
\mforall{}[T1,T2:Type].  \mforall{}[f:T1  {}\mrightarrow{}  T2].  \mforall{}[bs:bag(T1)].
    uiff(bag-no-repeats(T2;bag-map(f;bs));bag-no-repeats(T1;bs))  supposing  Inj(T1;T2;f)


By

---

Latex:
(Unfold  `bag-no-repeats`  0
  THEN  Auto
  THEN  Unhide
  THEN  Auto
  THEN  SquashExRepD
  THEN  (BagToList  4  THEN  Auto)
  THEN  All  (Unfold  `bag-map`))

---

Home Index