### Nuprl 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)`

Proof

Definitions occuring in Statement :  locl-pre-preserving: `f is locl-pre-preserving on P` es-E: `E` event_ordering: `EO` compose: `f o g` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ─→ B[x]`
Lemmas :  locl-pre-preserving_wf subtype_rel_dep_function es-E_wf set_wf event_ordering_wf rel-pre-preserving-compose es-le_wf
\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)

Date html generated: 2015_07_17-AM-09_03_51
Last ObjectModification: 2015_01_27-PM-00_52_24

Home Index