---

Step * of Lemma is-filter-image-sq

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(Top)]. ∀[e:E].  (e ∈b f[X] ~ e ∈b X ∧b (#(f X(e)) =z 1))
BY
{ (RepUR ``es-filter-image eclass in-eclass eclass-val 
           eclass-compose1 `` 0⋅
   THEN (UnivCD THENA Auto)
   THEN AutoSplit) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[f:Top].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    (e  \mmember{}\msubb{}  f[X]  \msim{}  e  \mmember{}\msubb{}  X  \mwedge{}\msubb{}  (\#(f  X(e))  =\msubz{}  1))


By

(RepUR  ``es-filter-image  eclass  in-eclass  eclass-val 
                  eclass-compose1  ``  0\mcdot{}
  THEN  (UnivCD  THENA  Auto)
  THEN  AutoSplit)

---

Home Index