---

Step * of Lemma sub-bag-filter

∀[T:Type]. ∀p:T ⟶ 𝔹. ∀b,c:bag(T).  (sub-bag(T;b;[x∈c|p[x]]) ⇐⇒ sub-bag(T;b;c) ∧ (∀x:T. (x ↓∈ b ⇒ (↑p[x]))))
BY
{ ((UnivCD THENA Auto) THEN D 0 THEN Auto) }

1
1. [T] : Type
2. p : T ⟶ 𝔹
3. b : bag(T)
4. c : bag(T)
5. sub-bag(T;b;[x∈c|p[x]])
⊢ sub-bag(T;b;c)

2
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]

3
1. [T] : Type
2. p : T ⟶ 𝔹
3. b : bag(T)
4. c : bag(T)
5. sub-bag(T;b;c)
6. ∀x:T. (x ↓∈ b ⇒ (↑p[x]))
⊢ sub-bag(T;b;[x∈c|p[x]])

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  0  THEN  Auto)

---

Home Index