Step
*
of Lemma
bag-count-filter
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)]. ((#x in [t∈bs|p[t]]) ≤ (#x in bs))
BY
{ xxx(BasicUniformUnivCD Auto THEN Unhide)xxx }
1
.....wf.....
1. T : Type
2. p : T ⟶ 𝔹
3. eq : EqDecider(T)
4. x : T
5. bs : bag(T)
⊢ (#x in [t∈bs|p[t]]) ∈ ℤ
2
.....wf.....
1. T : Type
2. p : T ⟶ 𝔹
3. eq : EqDecider(T)
4. x : T
5. bs : bag(T)
⊢ (#x in bs) ∈ ℤ
3
1. T : Type
2. p : T ⟶ 𝔹
3. eq : EqDecider(T)
4. x : T
5. bs : bag(T)
⊢ (#x in [t∈bs|p[t]]) ≤ (#x in bs)
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[p:T {}\mrightarrow{} \mBbbB{}]. \mforall{}[eq:EqDecider(T)]. \mforall{}[x:T]. \mforall{}[bs:bag(T)].
((\#x in [t\mmember{}bs|p[t]]) \mleq{} (\#x in bs))
By
Latex:
xxx(BasicUniformUnivCD Auto THEN Unhide)xxx
Home
Index