---

Step * of Lemma es-E-filter-image

∀[Info,A:Type]. ∀[f:A ─→ bag(Top)]. ∀[es:EO+(Info)]. ∀[X:EClass(A)].  (E(f[X]) ⊆r E(X))
BY
{ Auto }

1
1. Info : Type
2. A : Type
3. f : A ─→ bag(Top)
4. es : EO+(Info)
5. X : EClass(A)
⊢ E(f[X]) ⊆r E(X)

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(Top)].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].    (E(f[X])  \msubseteq{}r  E(X))


By

Auto

---

Home Index