---

Step * of Lemma embedding-preserves-local-property

∀[Info:Type]. ∀[P:Id ─→ Info List+ ─→ ℙ].
  ∀eo1,eo2:EO+(Info). ∀f:E ─→ E.
    (es-local-embedding(Info;eo1;eo2;f)
    ⇒ (∀[e:E]. (es-local-property(i,L.P[i;L];eo1;e) ⇐⇒ es-local-property(i,L.P[i;L];eo2;f e))))
BY
{ (Auto
   THEN ParallelLast
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN (EqTypeCD ORELSE EqCD)
   THEN Auto
   THEN Try ((Symmetry THEN Complete (Auto)))
   THEN Unfold `es-le-before` 0
   THEN Auto') }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[P:Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}eo1,eo2:EO+(Info).  \mforall{}f:E  {}\mrightarrow{}  E.
        (es-local-embedding(Info;eo1;eo2;f)
        {}\mRightarrow{}  (\mforall{}[e:E].  (es-local-property(i,L.P[i;L];eo1;e)  \mLeftarrow{}{}\mRightarrow{}  es-local-property(i,L.P[i;L];eo2;f  e))))


By

(Auto
  THEN  ParallelLast
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  (EqTypeCD  ORELSE  EqCD)
  THEN  Auto
  THEN  Try  ((Symmetry  THEN  Complete  (Auto)))
  THEN  Unfold  `es-le-before`  0
  THEN  Auto')

---

Home Index