Nuprl Lemma : Q-R-pre-preserving-compose
∀es:EO
∀[P1,P2:E ─→ ℙ]. ∀[Q1,Q2,Q3:E ─→ E ─→ ℙ].
∀f1:{e:E| P1 e} ─→ {e:E| P2 e} . ∀f2:{e:E| P2 e} ─→ E.
(f1 is Q2-Q3-pre-preserving on P1 ⇒ f2 is Q1-Q2-pre-preserving on P2 ⇒ f2 o f1 is Q1-Q3-pre-preserving on P1)
Proof
Definitions occuring in Statement :
Q-R-pre-preserving: f is Q-R-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,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x]
Lemmas :
set_wf,
es-E_wf,
all_wf,
event_ordering_wf
\mforall{}es:EO
\mforall{}[P1,P2:E {}\mrightarrow{} \mBbbP{}]. \mforall{}[Q1,Q2,Q3:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}].
\mforall{}f1:\{e:E| P1 e\} {}\mrightarrow{} \{e:E| P2 e\} . \mforall{}f2:\{e:E| P2 e\} {}\mrightarrow{} E.
(f1 is Q2-Q3-pre-preserving on P1
{}\mRightarrow{} f2 is Q1-Q2-pre-preserving on P2
{}\mRightarrow{} f2 o f1 is Q1-Q3-pre-preserving on P1)
Date html generated:
2015_07_17-AM-09_03_12
Last ObjectModification:
2015_01_27-PM-00_54_09
Home
Index