---

Step * of Lemma es-is-filter-image

∀[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
{ ((UnivCD THENA Auto) THEN (RWO "is-filter-image-sq" 0⋅ THENA Auto) THEN AutoBoolCase ⌈e ∈b X⌉⋅ THEN Auto) }

---

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

((UnivCD  THENA  Auto)
  THEN  (RWO  "is-filter-image-sq"  0\mcdot{}  THENA  Auto)
  THEN  AutoBoolCase  \mkleeneopen{}e  \mmember{}\msubb{}  X\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index