---

Step * 1 1 of Lemma detach_msubset


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)) ∈ ℤ
BY
{ ((RWH (LemmaC `ndiff_add_eq_imax`) 0 
THENM RWH (LemmaC `count_bsubmset`) 4) THENA Auto) }

1
1. s : DSet
2. a : MSet{s}
3. b : MSet{s}
4. ∀x:|s|. ((x #∈ a) ≤ (x #∈ b))
5. x : |s|
⊢ (x #∈ b) = imax(x #∈ b;x #∈ a) ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
((RWH  (LemmaC  `ndiff\_add\_eq\_imax`)  0 
THENM  RWH  (LemmaC  `count\_bsubmset`)  4)  THENA  Auto)

---

Home Index