---

Step * 3 of Lemma fset_of_mset_count_bound


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

1
1. s : DSet
2. c : |s|
3. x : |s|
⊢ (c #∈ mset_inj{s}(x)) ≤ 1

---

Latex:

---

Latex:

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


By

---

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

---

Home Index