---

Step * of Lemma map-class_functionality

∀[Info,T,A,B:Type]. ∀[f:A ─→ T]. ∀[g:B ─→ T]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (f[a] where a from X) = (g[b] where b from 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)] ∈ T)))
BY
{ (Auto
   THEN BLemma `es-interface-extensionality`
   THEN Auto
   THEN Try (((RWO "is-map-class" (-1) THENM RWW "is-map-class" 0)
              THEN Auto
              THEN (RWO "map-class-val" 0 THEN Auto)⋅
              THEN (RWO "is-map-class" 0 THEN Auto)⋅))⋅) }

1
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))

2
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))

---

Latex:


\mforall{}[Info,T,A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  T].  \mforall{}[g:B  {}\mrightarrow{}  T].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    (f[a]  where  a  from  X)  =  (g[b]  where  b  from  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  BLemma  `es-interface-extensionality`
  THEN  Auto
  THEN  Try  (((RWO  "is-map-class"  (-1)  THENM  RWW  "is-map-class"  0)
                        THEN  Auto
                        THEN  (RWO  "map-class-val"  0  THEN  Auto)\mcdot{}
                        THEN  (RWO  "is-map-class"  0  THEN  Auto)\mcdot{}))\mcdot{})

---

Home Index