Nuprl Lemma : es-fwd-propagation-via-unique
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X,Y:EClass(T)]. ∀[f,g:E(X) ⟶ E(Y)].
(f = g ∈ (E(X) ⟶ E(Y))) supposing
(Surj(E(X);E(Y);g) and
Surj(E(X);E(Y);f) and
g:X ⇒ Y:T and
f:X ⇒ Y:T and
(∀y1,y2:E(Y). (loc(y1) = loc(y2) ∈ Id)) and
(∀x1,x2:E(X). (loc(x1) = loc(x2) ∈ Id)))
Proof
Definitions occuring in Statement :
es-fwd-propagation-via: f:X ⇒ Y:T,
es-E-interface: E(X),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-loc: loc(e),
Id: Id,
surject: Surj(A;B;f),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
es-fwd-propagation-via: f:X ⇒ Y:T,
and: P ∧ Q,
all: ∀x:A. B[x],
subtype_rel: A ⊆r B,
strongwellfounded: SWellFounded(R[x; y]),
exists: ∃x:A. B[x],
nat: ℕ,
implies: P ⇒ Q,
false: False,
ge: i ≥ j ,
satisfiable_int_formula: satisfiable_int_formula(fmla),
not: ¬A,
top: Top,
prop: ℙ,
guard: {T},
es-E-interface: E(X),
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
int_seg: {i..j-},
lelt: i ≤ j < k,
le: A ≤ B,
less_than': less_than'(a;b),
decidable: Dec(P),
or: P ∨ Q,
less_than: a < b,
squash: ↓T,
so_lambda: λ2x.t[x],
so_apply: x[s],
surject: Surj(A;B;f),
sq_type: SQType(T),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
es-locl: (e <loc e'),
es-locl-op: LocalOrderPreserving(f),
order-preserving: order-preserving(A;B;a1,a2.R1[a1; a2];b1,b2.R2[b1; b2];f),
label: ...$L... t,
inject: Inj(A;B;f)
Latex:
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[T:Type]. \mforall{}[X,Y:EClass(T)]. \mforall{}[f,g:E(X) {}\mrightarrow{} E(Y)].
(f = g) supposing
(Surj(E(X);E(Y);g) and
Surj(E(X);E(Y);f) and
g:X {}\mRightarrow{} Y:T and
f:X {}\mRightarrow{} Y:T and
(\mforall{}y1,y2:E(Y). (loc(y1) = loc(y2))) and
(\mforall{}x1,x2:E(X). (loc(x1) = loc(x2))))
Date html generated:
2016_05_17-AM-06_45_00
Last ObjectModification:
2016_01_17-PM-06_38_58
Theory : event-ordering
Home
Index