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
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
implies: P ⇒ Q,
so_apply: x[s1;s2;s3],
so_lambda: λ2x y.t[x; y],
subtype_rel: A ⊆r B,
so_apply: x[s1;s2],
es-E-interface: E(X),
top: Top,
sq_type: SQType(T),
guard: {T},
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
iff: P ⇐⇒ Q,
and: P ∧ Q,
prop: ℙ,
so_lambda: so_lambda(x,y,z.t[x; y; z]),
rev_implies: P ⇐ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
es-class-causal-rel: es-class-causal-rel,
exists: ∃x:A. B[x],
biject: Bij(A;B;f),
inject: Inj(A;B;f),
surject: Surj(A;B;f),
pi1: fst(t),
cand: A c∧ B,
squash: ↓T
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:
2016_05_17-AM-08_16_21
Last ObjectModification:
2016_01_17-PM-02_36_35
Theory : event-ordering
Home
Index