Nuprl Lemma : loc-ordered-filter
∀es:EO. ∀as:E List. (loc-ordered(es;as)
⇒ (∀P:{e:E| (e ∈ as)} ⟶ 𝔹. loc-ordered(es;filter(P;as))))
Proof
Definitions occuring in Statement :
loc-ordered: loc-ordered(es;L)
,
es-E: E
,
event_ordering: EO
,
l_member: (x ∈ l)
,
filter: filter(P;l)
,
list: T List
,
bool: 𝔹
,
all: ∀x:A. B[x]
,
implies: P
⇒ Q
,
set: {x:A| B[x]}
,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x]
,
implies: P
⇒ Q
,
uall: ∀[x:A]. B[x]
,
member: t ∈ T
,
loc-ordered: loc-ordered(es;L)
,
l-ordered: l-ordered(T;x,y.R[x; y];L)
,
prop: ℙ
,
iff: P
⇐⇒ Q
,
and: P ∧ Q
Latex:
\mforall{}es:EO. \mforall{}as:E List. (loc-ordered(es;as) {}\mRightarrow{} (\mforall{}P:\{e:E| (e \mmember{} as)\} {}\mrightarrow{} \mBbbB{}. loc-ordered(es;filter(P;as)))\000C)
Date html generated:
2016_05_16-AM-09_18_50
Last ObjectModification:
2015_12_28-PM-09_56_29
Theory : new!event-ordering
Home
Index