---

Step * 2 of Lemma map-class_functionality


1. Info : Type
2. T : Type
3. A : Type
4. B : Type
5. f : A ─→ T
6. g : B ─→ 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)] ∈ T)))
⊢ Singlevalued((f[a] where a from X))
BY
{ (ProveSV THEN Auto)⋅ }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  A  :  Type
4.  B  :  Type
5.  f  :  A  {}\mrightarrow{}  T
6.  g  :  B  {}\mrightarrow{}  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{}  Singlevalued((f[a]  where  a  from  X))


By

(ProveSV  THEN  Auto)\mcdot{}

---

Home Index