---

Step * of Lemma sv-class-iff

∀[Info:Type]. ∀[A:es:EO+(Info) ─→ E ─→ Type]. ∀[X:EClass(A[es;e])].
  (Singlevalued(X) ⇐⇒ ∀es:EO+(Info). ∀e:E.  ((X es e) = if (#(X es e) =z 1) then X es e else {} fi  ∈ bag(A[es;e])))
BY
{ Auto }

1
1. Info : Type
2. A : es:EO+(Info) ─→ E ─→ Type
3. X : EClass(A[es;e])
4. Singlevalued(X)@i'
5. es : EO+(Info)@i'
6. e : E@i
⊢ (X es e) = if (#(X es e) =z 1) then X es e else {} fi  ∈ bag(A[es;e])

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

---

Latex:


\mforall{}[Info:Type].  \mforall{}[A:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type].  \mforall{}[X:EClass(A[es;e])].
    (Singlevalued(X)
    \mLeftarrow{}{}\mRightarrow{}  \mforall{}es:EO+(Info).  \mforall{}e:E.    ((X  es  e)  =  if  (\#(X  es  e)  =\msubz{}  1)  then  X  es  e  else  \{\}  fi  ))


By

Auto

---

Home Index