---

Step * 2 of Lemma sub-bag-filter


1. T : Type
2. p : T ⟶ 𝔹
3. b : bag(T)
4. c : bag(T)
5. sub-bag(T;b;[x∈c|p[x]])
6. sub-bag(T;b;c)
7. x : T
8. x ↓∈ b
⊢ ↑p[x]
BY
{ ((FLemma `sub-bag-member` [-1;-4] THENA Auto) THEN RWO "bag-member-filter" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  p  :  T  {}\mrightarrow{}  \mBbbB{}
3.  b  :  bag(T)
4.  c  :  bag(T)
5.  sub-bag(T;b;[x\mmember{}c|p[x]])
6.  sub-bag(T;b;c)
7.  x  :  T
8.  x  \mdownarrow{}\mmember{}  b
\mvdash{}  \muparrow{}p[x]


By

---

Latex:
((FLemma  `sub-bag-member`  [-1;-4]  THENA  Auto)  THEN  RWO  "bag-member-filter"  (-1)  THEN  Auto)

---

Home Index