Step
*
of Lemma
prod_in_mset_prod
∀g:DMon. ∀a,b:MSet{g↓set}. ∀u,v:|g|. ((↑(u ∈b a))
⇒ (↑(v ∈b b))
⇒ (↑((u * v) ∈b a × b)))
BY
{ ((RepD THENM Unfold `mset_prod` 0) THENA Auto) }
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)
⊢ ↑((u * v)
∈b msFor{<MSet{g↓set},⋃,0>} u ∈ a
msFor{<MSet{g↓set},⋃,0>} v ∈ b
mset_inj{g↓set}(u * v))
Latex:
Latex:
\mforall{}g:DMon. \mforall{}a,b:MSet\{g\mdownarrow{}set\}. \mforall{}u,v:|g|. ((\muparrow{}(u \mmember{}\msubb{} a)) {}\mRightarrow{} (\muparrow{}(v \mmember{}\msubb{} b)) {}\mRightarrow{} (\muparrow{}((u * v) \mmember{}\msubb{} a \mtimes{} b)))
By
Latex:
((RepD THENM Unfold `mset\_prod` 0) THENA Auto)
Home
Index