---

Step * 1 of Lemma bsublist_weakening


1. s : DSet@i'
2. as : |s| List@i
3. bs : |s| List@i
4. as ≡(|s|) bs@i
⊢ ↑bsublist(s;as;bs)
BY
{ ((FLemma `permr_iff_eq_counts_a` [4] THENM BLemma `count_bsublist`) THENA Auto) }

1
1. s : DSet@i'
2. as : |s| List@i
3. bs : |s| List@i
4. as ≡(|s|) bs@i
5. ∀x:|s|. ((x #∈ as) = (x #∈ bs) ∈ ℤ)
⊢ ∀c:|s|. ((c #∈ as) ≤ (c #∈ bs))

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  as  :  |s|  List@i
3.  bs  :  |s|  List@i
4.  as  \mequiv{}(|s|)  bs@i
\mvdash{}  \muparrow{}bsublist(s;as;bs)


By

---

Latex:
((FLemma  `permr\_iff\_eq\_counts\_a`  [4]  THENM  BLemma  `count\_bsublist`)  THENA  Auto)

---

Home Index