---

Step * 1 of Lemma filter-image_functionality


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))
BY
{ RepeatFor 2 ((Ext THEN Auto THEN Try ((Fold `eclass` 0 THEN Auto)))) }

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))))
10. x : EO+(Info)
11. x1 : E
⊢ (f[X] x x1) = (g[Y] x x1) ∈ bag(T)

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  A  :  Type
4.  B  :  Type
5.  f  :  A  {}\mrightarrow{}  bag(T)
6.  g  :  B  {}\mrightarrow{}  bag(T)
7.  X  :  EClass(A)
8.  Y  :  EClass(B)
9.  \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)))))
\mvdash{}  f[X]  =  g[Y]


By

RepeatFor  2  ((Ext  THEN  Auto  THEN  Try  ((Fold  `eclass`  0  THEN  Auto))))

---

Home Index