---

Step * of Lemma mset_map_char

∀s,s':DSet. ∀f:|s| ⟶ |s'|. ∀as:|s| List.  (msmap{s,s'}(f;mk_mset(as)) = mk_mset(map(f;as)) ∈ MSet{s'})
BY
{ (InductionOnListA THEN Reduce 0) }

1
1. s : DSet
2. s' : DSet
3. f : |s| ⟶ |s'|
⊢ msmap{s,s'}(f;mk_mset([])) = mk_mset([]) ∈ MSet{s'}

2
1. s : DSet
2. s' : DSet
3. f : |s| ⟶ |s'|
4. a : |s|
5. as : |s| List
6. msmap{s,s'}(f;mk_mset(as)) = mk_mset(map(f;as)) ∈ MSet{s'}
⊢ msmap{s,s'}(f;mk_mset([a / as])) = mk_mset([f a / map(f;as)]) ∈ MSet{s'}

---

Latex:

---

Latex:
\mforall{}s,s':DSet.  \mforall{}f:|s|  {}\mrightarrow{}  |s'|.  \mforall{}as:|s|  List.    (msmap\{s,s'\}(f;mk\_mset(as))  =  mk\_mset(map(f;as)))


By

---

Latex:
(InductionOnListA  THEN  Reduce  0)

---

Home Index