---

Step * of Lemma bag-filter-same

∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  [x∈bs|p[x]] = bs ∈ bag(T) supposing ∀x:T. (x ↓∈ bs ⇒ (↑p[x]))
BY
{ (Auto
   THEN (InstLemma `bag-filter-trivial` [⌜{x:T| x ↓∈ bs} ⌝;⌜p⌝]⋅ THENA (Auto THEN D (-1) THEN Unhide THEN Auto))
   THEN (InstHyp [⌜bs⌝] (-1)⋅ THENA (BLemma `bag-settype` THEN Auto))) }

1
1. T : Type
2. p : T ⟶ 𝔹
3. bs : bag(T)
4. ∀x:T. (x ↓∈ bs ⇒ (↑p[x]))
5. ∀[bs@0:bag({x:T| x ↓∈ bs} )]. ([x∈bs@0|p[x]] = bs@0 ∈ bag({x:T| x ↓∈ bs} ))
6. [x∈bs|p[x]] = bs ∈ bag({x:T| x ↓∈ bs} )
⊢ [x∈bs|p[x]] = bs ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].    [x\mmember{}bs|p[x]]  =  bs  supposing  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  (\muparrow{}p[x]))


By

---

Latex:
(Auto
  THEN  (InstLemma  `bag-filter-trivial`  [\mkleeneopen{}\{x:T|  x  \mdownarrow{}\mmember{}  bs\}  \mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  (-1)  THEN  Unhide  THEN  Auto)
              )
  THEN  (InstHyp  [\mkleeneopen{}bs\mkleeneclose{}]  (-1)\mcdot{}  THENA  (BLemma  `bag-settype`  THEN  Auto)))

---

Home Index