---

Step * of Lemma sub-mset-map

∀[A,B:Type].  ∀f:A ⟶ B. ∀L1,L2:A List.  (sub-mset(A; L1; L2) ⇒ sub-mset(B; map(f;L1); map(f;L2)))
BY
{ (Auto THEN All (Unfold `sub-mset`)⋅ THEN ExRepD THEN With ⌜map(f;L)⌝ (D 0)⋅ THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. f : A ⟶ B@i
4. L1 : A List@i
5. L2 : A List@i
6. L : A List@i
7. permutation(A;L @ L1;L2)@i
⊢ permutation(B;map(f;L) @ map(f;L1);map(f;L2))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}L1,L2:A  List.    (sub-mset(A;  L1;  L2)  {}\mRightarrow{}  sub-mset(B;  map(f;L1);  map(f;L2)))


By

---

Latex:
(Auto  THEN  All  (Unfold  `sub-mset`)\mcdot{}  THEN  ExRepD  THEN  With  \mkleeneopen{}map(f;L)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index