---

Step * 1 1 of Lemma locl-pre-preserving-compose


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
8. f2 o f1 is λe,e'. e ≤loc e' -pre-preserving on P
⊢ f2 o f1 is locl-pre-preserving on P
BY
{ (Fold `locl-pre-preserving` (-1) THEN Trivial) }

---

Latex:



1.  es  :  EO@i'
2.  [P]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  f1  :  \{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  @i
5.  f2  :  \{e:E|  Q  e\}    {}\mrightarrow{}  E@i
6.  f1  is  locl-pre-preserving  on  P@i
7.  f2  is  locl-pre-preserving  on  Q@i
8.  f2  o  f1  is  \mlambda{}e,e'.  e  \mleq{}loc  e'  -pre-preserving  on  P
\mvdash{}  f2  o  f1  is  locl-pre-preserving  on  P


By

(Fold  `locl-pre-preserving`  (-1)  THEN  Trivial)

---

Home Index