Nuprl Lemma : embedding-preserves-local-class
∀[Info,A:Type]. ∀[X:EClass(A)].
(LocalClass(X)
⇒ (∀eo1,eo2:EO+(Info). ∀f:E ─→ E.
(es-local-embedding(Info;eo1;eo2;f) ⇒ (∀[e:E]. ∀[v:A]. (v ∈ X(e) ⇐⇒ v ∈ X(f e))))))
Proof
Definitions occuring in Statement :
local-class: LocalClass(X),
classrel: v ∈ X(e),
eclass: EClass(A[eo; e]),
es-local-embedding: es-local-embedding(Info;eo1;eo2;f),
event-ordering+: EO+(Info),
es-E: E,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type
Lemmas :
bag-member_wf,
squash_wf,
true_wf,
bag_wf,
iff_weakening_equal,
pi2_wf,
hdataflow_wf,
hdf-ap_wf,
map_append_sq,
general-append-cancellation,
map_cons_lemma,
map_nil_lemma,
map_wf,
es-E_wf,
event-ordering+_subtype,
es-info_wf,
es-before_wf,
cons_wf,
nil_wf,
length_wf,
equal_wf,
iterate-hdataflow_wf,
reduce_hd_cons_lemma,
hd_wf,
ge_wf,
listp_properties,
cons_wf_listp,
classrel_wf,
es-local-embedding_wf,
event-ordering+_wf,
local-class_wf,
eclass_wf
\mforall{}[Info,A:Type]. \mforall{}[X:EClass(A)].
(LocalClass(X)
{}\mRightarrow{} (\mforall{}eo1,eo2:EO+(Info). \mforall{}f:E {}\mrightarrow{} E.
(es-local-embedding(Info;eo1;eo2;f) {}\mRightarrow{} (\mforall{}[e:E]. \mforall{}[v:A]. (v \mmember{} X(e) \mLeftarrow{}{}\mRightarrow{} v \mmember{} X(f e))))))
Date html generated:
2015_07_17-PM-00_31_55
Last ObjectModification:
2015_02_04-PM-05_32_24
Home
Index