---

Step * 1 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((g[b] where b from Y))
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((g[b]  where  b  from  Y))


By

(ProveSV  THEN  Auto)

---

Home Index