---

Step * 1 1 1 of Lemma prod_in_mset_prod


1. g : DMon
2. a : MSet{g↓set}
3. b : MSet{g↓set}
4. u : |g|
5. v : |g|
6. ↑(u
∈b a)
7. ↑(v
∈b b)
⊢ ∃u1:|(g↓set)|. ((↑(u1 ∈b a)) ∧ (↑(∃b{g↓set} v1 ∈ b. ((u * v) ∈b mset_inj{g↓set}(u1 * v1)))))
BY
{ xxx(With ⌜u⌝ (D 0)⋅ THEN Auto THEN ((BLemma `bmsexists_char` THENA Auto) THEN With ⌜v⌝ (D 0)⋅ THEN Auto))xxx }

1
1. g : DMon
2. a : MSet{g↓set}
3. b : MSet{g↓set}
4. u : |g|
5. v : |g|
6. ↑(u
∈b a)
7. ↑(v
∈b b)
8. ↑(u
∈b a)
9. ↑(v
∈b b)
⊢ ↑((u * v)
∈b mset_inj{g↓set}(u * v))

---

Latex:

---

Latex:

1.  g  :  DMon
2.  a  :  MSet\{g\mdownarrow{}set\}
3.  b  :  MSet\{g\mdownarrow{}set\}
4.  u  :  |g|
5.  v  :  |g|
6.  \muparrow{}(u
\mmember{}\msubb{}  a)
7.  \muparrow{}(v
\mmember{}\msubb{}  b)
\mvdash{}  \mexists{}u1:|(g\mdownarrow{}set)|.  ((\muparrow{}(u1  \mmember{}\msubb{}  a))  \mwedge{}  (\muparrow{}(\mexists{}\msubb{}\{g\mdownarrow{}set\}  v1  \mmember{}  b.  ((u  *  v)  \mmember{}\msubb{}  mset\_inj\{g\mdownarrow{}set\}(u1  *  v1)))))


By

---

Latex:
xxx(With  \mkleeneopen{}u\mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto
        THEN  ((BLemma  `bmsexists\_char`  THENA  Auto)  THEN  With  \mkleeneopen{}v\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))xxx

---

Home Index