---

Step * 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)
⊢ ↑(∃b{g↓set} u1 ∈ a
               ∃b{g↓set} v1 ∈ b
                          ((u * v)
                         ∈b mset_inj{g↓set}(u1 * v1)))
BY
{ xxx(BLemma `bmsexists_char` THENA 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)
⊢ ∃u1:|(g↓set)|. ((↑(u1 ∈b a)) ∧ (↑(∃b{g↓set} v1 ∈ b. ((u * v) ∈b mset_inj{g↓set}(u1 * v1)))))

---

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{}  \muparrow{}(\mexists{}\msubb{}\{g\mdownarrow{}set\}  u1  \mmember{}  a
                              \mexists{}\msubb{}\{g\mdownarrow{}set\}  v1  \mmember{}  b
                                                    ((u  *  v)
                                                  \mmember{}\msubb{}  mset\_inj\{g\mdownarrow{}set\}(u1  *  v1)))


By

---

Latex:
xxx(BLemma  `bmsexists\_char`  THENA  Auto)xxx

---

Home Index