---

Step * of Lemma sub-bag-filter3

∀T:Type. ∀p:T ⟶ 𝔹. ∀b,c:bag(T).  (sub-bag(T;b;c) ⇒ sub-bag(T;[x∈b|p[x]];[x∈c|p[x]]))
BY
{ (Auto THEN ParallelLast THEN ExRepD THEN With ⌜[x∈cs|p[x]]⌝ (D 0)⋅ THEN Auto) }

1
1. T : Type
2. p : T ⟶ 𝔹
3. b : bag(T)
4. c : bag(T)
5. cs : bag(T)
6. c = (b + cs) ∈ bag(T)
⊢ [x∈c|p[x]] = ([x∈b|p[x]] + [x∈cs|p[x]]) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}p:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}b,c:bag(T).    (sub-bag(T;b;c)  {}\mRightarrow{}  sub-bag(T;[x\mmember{}b|p[x]];[x\mmember{}c|p[x]]))


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  ExRepD  THEN  With  \mkleeneopen{}[x\mmember{}cs|p[x]]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index