---

Step * 1 of Lemma es-is-interface-filter


∀Info:Type. ∀es:EO+(Info). ∀A:Type. ∀X:EClass(A). ∀P:A ─→ 𝔹. ∀e:E.  (↑e ∈b X|a.P[a] ⇐⇒ {(↑e ∈b X) ∧ (↑P[X(e)])})
BY
{ (RepUR ``in-eclass eclass eclass-val eclass-compose1  
           es-interface-filter guard`` 0⋅
   THEN (UnivCD THENA Auto)
   ) }

1
1. Info : Type@i'
2. es : EO+(Info)@i'
3. A : Type@i'
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)@i'
5. P : A ─→ 𝔹@i
6. e : E@i
⊢ ↑(#(if (#(X es e) =z 1) then [a∈X es e|P[a]] else {} fi ) =z 1) ⇐⇒ (↑(#(X es e) =z 1)) ∧ (↑P[only(X es e)])

---

Latex:

---

Latex:

\mforall{}Info:Type.  \mforall{}es:EO+(Info).  \mforall{}A:Type.  \mforall{}X:EClass(A).  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}e:E.
    (\muparrow{}e  \mmember{}\msubb{}  X|a.P[a]  \mLeftarrow{}{}\mRightarrow{}  \{(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\muparrow{}P[X(e)])\})


By

---

Latex:
(RepUR  ``in-eclass  eclass  eclass-val  eclass-compose1   
                  es-interface-filter  guard``  0\mcdot{}
  THEN  (UnivCD  THENA  Auto)
  )

---

Home Index