---

Step * of Lemma filter-image_functionality

∀[Info,T,A,B:Type]. ∀[f:A ─→ bag(T)]. ∀[g:B ─→ bag(T)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  f[X] = g[Y] ∈ EClass(T) 
  supposing ∀es:EO+(Info). ∀e:E.  ((↑e ∈b X ⇐⇒ ↑e ∈b Y) ∧ ((↑e ∈b X) ⇒ (↑e ∈b Y) ⇒ ((f X(e)) = (g Y(e)) ∈ bag(T))))
BY
{ (Auto THEN Unfold `eclass` 0) }

1
1. Info : Type
2. T : Type
3. A : Type
4. B : Type
5. f : A ─→ bag(T)
6. g : B ─→ bag(T)
7. X : EClass(A)
8. Y : EClass(B)
9. ∀es:EO+(Info). ∀e:E.  ((↑e ∈b X ⇐⇒ ↑e ∈b Y) ∧ ((↑e ∈b X) ⇒ (↑e ∈b Y) ⇒ ((f X(e)) = (g Y(e)) ∈ bag(T))))
⊢ f[X] = g[Y] ∈ (es:EO+(Info) ─→ e:E ─→ bag(T))

---

Latex:


\mforall{}[Info,T,A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(T)].  \mforall{}[g:B  {}\mrightarrow{}  bag(T)].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    f[X]  =  g[Y] 
    supposing  \mforall{}es:EO+(Info).  \mforall{}e:E.
                            ((\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  Y)  \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  X)  {}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  Y)  {}\mRightarrow{}  ((f  X(e))  =  (g  Y(e)))))


By

(Auto  THEN  Unfold  `eclass`  0)

---

Home Index