---

Step * of Lemma es-is-filter-image2

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[X:EClass(A)]. ∀[e:E].
  uiff(↑e ∈b f[X];{(↑e ∈b X) ∧ (#(f X(e)) = 1 ∈ ℤ)})
BY
{ (InstLemma `es-is-filter-image` [] THEN Unfold `guard` 0 THEN Try (Trivial)) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    uiff(\muparrow{}e  \mmember{}\msubb{}  f[X];\{(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\#(f  X(e))  =  1)\})


By

---

Latex:
(InstLemma  `es-is-filter-image`  []  THEN  Unfold  `guard`  0  THEN  Try  (Trivial))

---

Home Index