---

Step * of Lemma es-interface-set-subtype

∀[Info,A:Type]. ∀[P:A ─→ ℙ]. ∀[X:EClass(A)].
  (X ∈ EClass({a:A| P[a]} )) supposing ((∀es:EO+(Info). ∀e:E(X).  P[X(e)]) and Singlevalued(X))
BY
{ WithCumulativity((Auto THEN All (Unfold `eclass`))) }

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)]
⊢ X ∈ es:EO+(Info) ─→ e:E ─→ bag({a:A| P[a]} )

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[X:EClass(A)].
    (X  \mmember{}  EClass(\{a:A|  P[a]\}  ))  supposing  ((\mforall{}es:EO+(Info).  \mforall{}e:E(X).    P[X(e)])  and  Singlevalued(X))


By

WithCumulativity((Auto  THEN  All  (Unfold  `eclass`)))

---

Home Index