---

Step * of Lemma es-interface-map-val

∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[f:A ⟶ E(X) ⟶ bag(Top)]. ∀[e:E].
  es-interface-map(f;X)(e) ~ only(f X(e) e) supposing ↑e ∈b es-interface-map(f;X)
BY
{ (BasicUniformUnivCD Auto
   THEN RepUR ``eclass-val in-eclass es-interface-map let`` 0
   THEN UseWitness ⌜Ax⌝⋅
   THEN AutoSplit) }

1
1. Info : Type
2. A : Type
3. es : EO+(Info)
4. X : EClass(A)
5. f : A ⟶ E(X) ⟶ bag(Top)
6. e : E
7. #(X es e) = 1 ∈ ℤ
⊢ Ax ∈ only(f only(X es e) e) ~ only(f only(X es e) e) supposing ↑(#(f only(X es e) e) =z 1)

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].  \mforall{}[f:A  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  bag(Top)].  \mforall{}[e:E].
    es-interface-map(f;X)(e)  \msim{}  only(f  X(e)  e)  supposing  \muparrow{}e  \mmember{}\msubb{}  es-interface-map(f;X)


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  RepUR  ``eclass-val  in-eclass  es-interface-map  let``  0
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  AutoSplit)

---

Home Index