---

Step * of Lemma is-interface-part

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[g:E(X) ─→ Id]. ∀[i:Id]. ∀[e:E].
  uiff(↑e ∈b (X|g=i);(↑e ∈b X) ∧ ((g e) = i ∈ Id))
BY
{ (RepUR ``in-eclass es-interface-part eclass es-E-interface let`` 0
   THEN BasicUniformUnivCD Auto
   THEN UseWitness ⌈<<Ax, Ax>, Ax>⌉⋅
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[g:E(X)  {}\mrightarrow{}  Id].  \mforall{}[i:Id].  \mforall{}[e:E].
    uiff(\muparrow{}e  \mmember{}\msubb{}  (X|g=i);(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  ((g  e)  =  i))


By

---

Latex:
(RepUR  ``in-eclass  es-interface-part  eclass  es-E-interface  let``  0
  THEN  BasicUniformUnivCD  Auto
  THEN  UseWitness  \mkleeneopen{}<<Ax,  Ax>,  Ax>\mkleeneclose{}\mcdot{}
  THEN  AutoSplit)

---

Home Index