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]
Definitions unfolded in proof :
compose: f o g,
Q-R-pre-preserving: f is Q-R-pre-preserving on P,
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
so_apply: x[s],
guard: {T}
Latex:
\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:
2016_05_16-AM-10_19_02
Last ObjectModification:
2015_12_28-PM-09_23_40
Theory : new!event-ordering
Home
Index