---

Step * of Lemma bag-combine-size-bound2

∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[L:bag(A)]. ∀[a:A].  #(f[a]) ≤ #(⋃a∈L.f[a]) supposing a ↓∈ L
BY
{ (Auto
   THEN (BagToList (-3) THENA Auto)
   THEN (FLemma `bag-member-sq-list-member` [-1] THENA Auto)
   THEN D (-1)
   THEN (Unhide THENA Auto)
   THEN Thin (-2)
   THEN Using [`a',⌜a⌝] (BLemma `bag-combine-size-bound`)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[L:bag(A)].  \mforall{}[a:A].    \#(f[a])  \mleq{}  \#(\mcup{}a\mmember{}L.f[a])  supposing  a  \mdownarrow{}\mmember{}  L


By

---

Latex:
(Auto
  THEN  (BagToList  (-3)  THENA  Auto)
  THEN  (FLemma  `bag-member-sq-list-member`  [-1]  THENA  Auto)
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  Thin  (-2)
  THEN  Using  [`a',\mkleeneopen{}a\mkleeneclose{}]  (BLemma  `bag-combine-size-bound`)\mcdot{}
  THEN  Auto)

---

Home Index