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