---

Step * 1 of Lemma mapfilter-class-val

.....wf..... 
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. P : A ─→ 𝔹
6. f : A ─→ B
7. X : es:EO+(Info) ─→ e:E ─→ bag(A)
8. e : E
9. #(X es e) = 1 ∈ ℤ
⊢ P[only(X es e)] ∈ 𝔹
BY
{ Auto }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. P : A ─→ 𝔹
6. f : A ─→ B
7. X : es:EO+(Info) ─→ e:E ─→ bag(A)
8. e : E
9. #(X es e) = 1 ∈ ℤ
⊢ single-valued-bag(X es e;A)

---

Latex:


.....wf..... 
1.  Info  :  Type
2.  es  :  EO+(Info)
3.  A  :  Type
4.  B  :  Type
5.  P  :  A  {}\mrightarrow{}  \mBbbB{}
6.  f  :  A  {}\mrightarrow{}  B
7.  X  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A)
8.  e  :  E
9.  \#(X  es  e)  =  1
\mvdash{}  P[only(X  es  e)]  \mmember{}  \mBbbB{}


By

Auto

---

Home Index