Nuprl Lemma : es-class-causal-rel-iff-bijection
∀[Info,A,B:Type].
∀es:EO+(Info). ∀X:EClass(A). ∀Y:EClass(B).
∀[R:E(X) ─→ A ─→ B ─→ ℙ]
(e∈X(x) ⇐c⇒ Y(y) such that
R[e;x;y]
⇐⇒ ∃f:E(X) ─→ E(Y). (Bij(E(X);E(Y);f) ∧ (∀e:E(X). (e c≤ f e ∧ R[e;X(e);Y(f e)])))) supposing
((∀b1,b2:E(Y). ∀e:E(X). (R[e;X(e);Y(b1)] ⇒ R[e;X(e);Y(b2)] ⇒ (b1 = b2 ∈ E(Y)))) and
(∀b:B. ∀a1,a2:E(X). (R[a1;X(a1);b] ⇒ R[a2;X(a2);b] ⇒ (a1 = a2 ∈ E(X)))))
Proof
Definitions occuring in Statement :
es-class-causal-rel: es-class-causal-rel,
es-E-interface: E(X),
eclass-val: X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-causle: e c≤ e',
biject: Bij(A;B;f),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
eclass-val_wf,
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
assert_elim,
in-eclass_wf,
es-interface-subtype_rel2,
top_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
es-E-interface_wf,
es-class-causal-rel_wf,
exists_wf,
biject_wf,
all_wf,
es-causle_wf,
es-E-interface-property,
eclass_wf,
equal_wf,
and_wf,
squash_wf,
assert_wf,
subtype_top,
event-ordering+_cumulative2
Latex:
\mforall{}[Info,A,B:Type].
\mforall{}es:EO+(Info). \mforall{}X:EClass(A). \mforall{}Y:EClass(B).
\mforall{}[R:E(X) {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}]
(e\mmember{}X(x) \mLeftarrow{}c\mRightarrow{} Y(y) such that
R[e;x;y]
\mLeftarrow{}{}\mRightarrow{} \mexists{}f:E(X) {}\mrightarrow{} E(Y)
(Bij(E(X);E(Y);f) \mwedge{} (\mforall{}e:E(X). (e c\mleq{} f e \mwedge{} R[e;X(e);Y(f e)])))) supposing
((\mforall{}b1,b2:E(Y). \mforall{}e:E(X). (R[e;X(e);Y(b1)] {}\mRightarrow{} R[e;X(e);Y(b2)] {}\mRightarrow{} (b1 = b2))) and
(\mforall{}b:B. \mforall{}a1,a2:E(X). (R[a1;X(a1);b] {}\mRightarrow{} R[a2;X(a2);b] {}\mRightarrow{} (a1 = a2))))
Date html generated:
2015_07_21-PM-04_25_59
Last ObjectModification:
2015_01_27-PM-05_21_38
Home
Index