---

Step * 1 of Lemma es-interface-set-subtype


1. Info : Type
2. A : Type
3. P : A ─→ ℙ
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(X)
6. ∀es:EO+(Info). ∀e:E(X).  P[X(e)]
⊢ X ∈ es:EO+(Info) ─→ e:E ─→ bag({a:A| P[a]} )
BY
{ ((ExtWith [`eo'] [⌈eo:EO+(Info) ─→ E ─→ bag(A)⌉]⋅ THEN Try (Complete (Auto)))
   THEN ExtWith [`e'] [⌈E ─→ bag(A)⌉]⋅
   THEN Auto
   THEN (Assert #(X eo e) ≤ 1 BY
               Auto')) }

1
1. Info : Type
2. A : Type
3. P : A ─→ ℙ
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(X)
6. ∀es:EO+(Info). ∀e:E(X).  P[X(e)]
7. eo : EO+(Info)
8. e : E
9. #(X eo e) ≤ 1
⊢ X eo e ∈ bag({a:A| P[a]} )

---

Latex:



1.  Info  :  Type
2.  A  :  Type
3.  P  :  A  {}\mrightarrow{}  \mBbbP{}
4.  X  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A)
5.  Singlevalued(X)
6.  \mforall{}es:EO+(Info).  \mforall{}e:E(X).    P[X(e)]
\mvdash{}  X  \mmember{}  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(\{a:A|  P[a]\}  )


By

((ExtWith  [`eo']  [\mkleeneopen{}eo:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  bag(A)\mkleeneclose{}]\mcdot{}  THEN  Try  (Complete  (Auto)))
  THEN  ExtWith  [`e']  [\mkleeneopen{}E  {}\mrightarrow{}  bag(A)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (Assert  \#(X  eo  e)  \mleq{}  1  BY
                          Auto'))

---

Home Index