---

Step * 1 of Lemma bag-count-map

.....antecedent..... 
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ T2
4. eq1 : EqDecider(T1)
5. eq2 : EqDecider(T2)
6. ∀[x:T1]. ∀[bs:bag(T1)].  (#f x in bag-map(f;bs)) ~ (#x in bs) supposing Inj(T1;T2;f)
7. x : T2
8. bs : bag(T1)
9. g : T2 ⟶ T1
10. ∀x:T2. ((f (g x)) = x ∈ T2)
11. ∀x:T1. ((g (f x)) = x ∈ T1)
⊢ Inj(T1;T2;f)
BY
{ ((D 0 THEN Auto) THEN (InstHyp[⌜a1⌝] 11⋅ THENA Auto) THEN (InstHyp[⌜a2⌝] 11⋅ THENA Auto) THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T1  :  Type
2.  T2  :  Type
3.  f  :  T1  {}\mrightarrow{}  T2
4.  eq1  :  EqDecider(T1)
5.  eq2  :  EqDecider(T2)
6.  \mforall{}[x:T1].  \mforall{}[bs:bag(T1)].    (\#f  x  in  bag-map(f;bs))  \msim{}  (\#x  in  bs)  supposing  Inj(T1;T2;f)
7.  x  :  T2
8.  bs  :  bag(T1)
9.  g  :  T2  {}\mrightarrow{}  T1
10.  \mforall{}x:T2.  ((f  (g  x))  =  x)
11.  \mforall{}x:T1.  ((g  (f  x))  =  x)
\mvdash{}  Inj(T1;T2;f)


By

---

Latex:
((D  0  THEN  Auto)  THEN  (InstHyp[\mkleeneopen{}a1\mkleeneclose{}]  11\mcdot{}  THENA  Auto)  THEN  (InstHyp[\mkleeneopen{}a2\mkleeneclose{}]  11\mcdot{}  THENA  Auto)  THEN  Auto)

---

Home Index