---

Step * 2 of Lemma sv-class-iff


1. Info : Type
2. A : es:EO+(Info) ─→ E ─→ Type
3. X : EClass(A[es;e])
4. ∀es:EO+(Info). ∀e:E.  ((X es e) = if (#(X es e) =z 1) then X es e else {} fi  ∈ bag(A[es;e]))@i'
⊢ Singlevalued(X)
BY
{ (D 0 THEN Auto THEN RWO  "4" 0 THEN Auto THEN AutoSplit) }

---

Latex:



1.  Info  :  Type
2.  A  :  es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type
3.  X  :  EClass(A[es;e])
4.  \mforall{}es:EO+(Info).  \mforall{}e:E.    ((X  es  e)  =  if  (\#(X  es  e)  =\msubz{}  1)  then  X  es  e  else  \{\}  fi  )@i'
\mvdash{}  Singlevalued(X)


By

(D  0  THEN  Auto  THEN  RWO    "4"  0  THEN  Auto  THEN  AutoSplit)

---

Home Index