---

Step * of Lemma is-map-class

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[f:Top]. ∀[X:EClass(Top)]. ∀[e:E].  (e ∈b (f[v] where v from X) ~ e ∈b X)
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `map-class` 0
   THEN (RWO "is-filter-image-sq" 0 THENA Auto)
   THEN Reduce 0
   THEN RWO "band-btrue" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[f:Top].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    (e  \mmember{}\msubb{}  (f[v]  where  v  from  X)  \msim{}  e  \mmember{}\msubb{}  X)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `map-class`  0
  THEN  (RWO  "is-filter-image-sq"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RWO  "band-btrue"  0
  THEN  Auto)

---

Home Index