---

Step * 2 of Lemma fset_of_mset_count_bound


1. s : DSet
2. c : |s|
⊢ (c #∈ fset_of_mset(s;0{s})) ≤ 1
BY
{ ((Unfold `fset_of_mset` 0  
THENM RW mset_for_normC 0  
THENM Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  c  :  |s|
\mvdash{}  (c  \#\mmember{}  fset\_of\_mset(s;0\{s\}))  \mleq{}  1


By

---

Latex:
((Unfold  `fset\_of\_mset`  0   
THENM  RW  mset\_for\_normC  0   
THENM  Reduce  0)  THEN  Auto)

---

Home Index