---

Step * 1 of Lemma detach_msubset


1. s : DSet
2. a : MSet{s}
3. b : MSet{s}
4. ↑(a ⊆b b)
⊢ b = ((b - a) + a) ∈ MSet{s}
BY
{ ((BLemma `eq_mset_iff_eq_counts` 
THENM D 0  
THENM RewriteWith [] ``mset_count_sum mset_count_diff`` 0 ) THEN Auto) }

1
1. s : DSet
2. a : MSet{s}
3. b : MSet{s}
4. ↑(a ⊆b b)
5. x : |s|
⊢ (x #∈ b) = (((x #∈ b) -- (x #∈ a)) + (x #∈ a)) ∈ ℤ

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  MSet\{s\}
3.  b  :  MSet\{s\}
4.  \muparrow{}(a  \msubseteq{}\msubb{}  b)
\mvdash{}  b  =  ((b  -  a)  +  a)


By

---

Latex:
((BLemma  `eq\_mset\_iff\_eq\_counts` 
THENM  D  0   
THENM  RewriteWith  []  ``mset\_count\_sum  mset\_count\_diff``  0  )  THEN  Auto)

---

Home Index