---

Step * of Lemma count-related-pairs

No Annotations
∀[T,S:Type]. ∀[K:T List]. ∀[L:S List]. ∀[R:T ⟶ S ⟶ 𝔹].
  (Σ(||filter(R t;L)|| | t ∈ K) = Σ(||filter(λt.(R t s);K)|| | s ∈ L) ∈ ℤ)
BY
{ ((Intros THEN (RWO "length-filter-lsum" 0 THENA Auto)) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T,S:Type].  \mforall{}[K:T  List].  \mforall{}[L:S  List].  \mforall{}[R:T  {}\mrightarrow{}  S  {}\mrightarrow{}  \mBbbB{}].
    (\mSigma{}(||filter(R  t;L)||  |  t  \mmember{}  K)  =  \mSigma{}(||filter(\mlambda{}t.(R  t  s);K)||  |  s  \mmember{}  L))


By

---

Latex:
((Intros  THEN  (RWO  "length-filter-lsum"  0  THENA  Auto))  THEN  Reduce  0  THEN  Auto)

---

Home Index