Step
*
of Lemma
bag-filter-filter2
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[q:{x:T| ↑p[x]} ⟶ 𝔹]. ∀[bs:bag(T)].
([x∈[x∈bs|p[x]]|q[x]] = [x∈bs|p[x] ∧b q[x]] ∈ bag({x:T| ↑(p[x] ∧b q[x])} ))
BY
{ ((UnivCD THENA Auto) THEN (BagToList (-1) THENA Try (Complete (Auto)))) }
1
1. T : Type
2. p : T ⟶ 𝔹
3. q : {x:T| ↑p[x]} ⟶ 𝔹
4. bs : T List
⊢ [x∈[x∈bs|p[x]]|q[x]] = [x∈bs|p[x] ∧b q[x]] ∈ bag({x:T| ↑(p[x] ∧b q[x])} )
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[p:T {}\mrightarrow{} \mBbbB{}]. \mforall{}[q:\{x:T| \muparrow{}p[x]\} {}\mrightarrow{} \mBbbB{}]. \mforall{}[bs:bag(T)].
([x\mmember{}[x\mmember{}bs|p[x]]|q[x]] = [x\mmember{}bs|p[x] \mwedge{}\msubb{} q[x]])
By
Latex:
((UnivCD THENA Auto) THEN (BagToList (-1) THENA Try (Complete (Auto))))
Home
Index