---

Step * of Lemma locl-pre-preserving-compose

∀es:EO
  ∀[P,Q:E ─→ ℙ].
    ∀f1:{e:E| P e}  ─→ {e:E| Q e} . ∀f2:{e:E| Q e}  ─→ E.
      ((f1 is locl-pre-preserving on P ∧ f2 is locl-pre-preserving on Q) ⇒ f2 o f1 is locl-pre-preserving on P)
BY
{ Auto }

1
1. es : EO@i'
2. [P] : E ─→ ℙ
3. [Q] : E ─→ ℙ
4. f1 : {e:E| P e}  ─→ {e:E| Q e} @i
5. f2 : {e:E| Q e}  ─→ E@i
6. f1 is locl-pre-preserving on P@i
7. f2 is locl-pre-preserving on Q@i
⊢ f2 o f1 is locl-pre-preserving on P

---

Latex:


\mforall{}es:EO
    \mforall{}[P,Q:E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f1:\{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  .  \mforall{}f2:\{e:E|  Q  e\}    {}\mrightarrow{}  E.
            ((f1  is  locl-pre-preserving  on  P  \mwedge{}  f2  is  locl-pre-preserving  on  Q)
            {}\mRightarrow{}  f2  o  f1  is  locl-pre-preserving  on  P)


By

Auto

---

Home Index