---

Step * of Lemma assert-is-filter-image

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(Top)]. ∀[e:E].
  (↑e ∈b f[X] ~ if e ∈b X then ↑(#(f X(e)) =z 1) else False fi )
BY
{ ((UnivCD THENA Auto) THEN (RWO "is-filter-image-sq" 0 THENA Auto) THEN AutoBoolCase ⌜e ∈b X⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[f:Top].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    (\muparrow{}e  \mmember{}\msubb{}  f[X]  \msim{}  if  e  \mmember{}\msubb{}  X  then  \muparrow{}(\#(f  X(e))  =\msubz{}  1)  else  False  fi  )


By

---

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

---

Home Index