---

Step * of Lemma embedding-preserves-local-class

∀[Info,A:Type]. ∀[X:EClass(A)].
  (LocalClass(X)
  ⇒ (∀eo1,eo2:EO+(Info). ∀f:E ─→ E.
        (es-local-embedding(Info;eo1;eo2;f) ⇒ (∀[e:E]. ∀[v:A].  (v ∈ X(e) ⇐⇒ v ∈ X(f e))))))
BY
{ (Auto
   THEN All (\h. Unfold `classrel` h THEN Fold `class-ap` h)
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN D 4
   THEN (RWO "5" 0  THENA Auto)
   THEN RepeatFor 2 ((EqCD THEN Auto))
   THEN (With ⌈e⌉ (D (-4))⋅ THENA Auto)
   THEN D -1
   THEN Unfold `es-le-before` -1
   THEN (RWO "map_append_sq" (-1) THENA Auto)
   THEN FLemma `general-append-cancellation` [-1]
   THEN Reduce (-1)
   THEN Auto) }

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].
    (LocalClass(X)
    {}\mRightarrow{}  (\mforall{}eo1,eo2:EO+(Info).  \mforall{}f:E  {}\mrightarrow{}  E.
                (es-local-embedding(Info;eo1;eo2;f)  {}\mRightarrow{}  (\mforall{}[e:E].  \mforall{}[v:A].    (v  \mmember{}  X(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  X(f  e))))))


By

(Auto
  THEN  All  (\mbackslash{}h.  Unfold  `classrel`  h  THEN  Fold  `class-ap`  h)
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  D  4
  THEN  (RWO  "5"  0    THENA  Auto)
  THEN  RepeatFor  2  ((EqCD  THEN  Auto))
  THEN  (With  \mkleeneopen{}e\mkleeneclose{}  (D  (-4))\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Unfold  `es-le-before`  -1
  THEN  (RWO  "map\_append\_sq"  (-1)  THENA  Auto)
  THEN  FLemma  `general-append-cancellation`  [-1]
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index