Nuprl Lemma : sv-classrel
∀[Info,A:Type]. ∀[X:EClass(A)].
(Singlevalued(X) ⇒ (∀es:EO+(Info). ∀e:E. ∀v:A. (v ∈ X(e) ⇐⇒ (↑e ∈b X) ∧ (v = X(e) ∈ A))))
Proof
Definitions occuring in Statement :
sv-class: Singlevalued(X),
eclass-val: X(e),
in-eclass: e ∈b X,
classrel: v ∈ X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-E: E,
assert: ↑b,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
universe: Type,
equal: s = t ∈ T
Lemmas :
es-E_wf,
event-ordering+_subtype,
event-ordering+_wf,
sv-class_wf,
in-eclass_wf,
dep-eclass_subtype_rel,
top_wf,
classrel_wf,
assert_wf,
eclass-val_wf,
eclass_wf,
bag_wf,
eq_int_wf,
bag-size_wf,
bool_wf,
eqtt_to_assert,
assert_of_eq_int,
nat_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_int,
bag-size-one,
bag-only_wf2,
decidable__lt,
false_wf,
le_antisymmetry_iff,
add_functionality_wrt_le,
add-zero,
le-add-cancel,
single-valued-bag-if-le1,
le_weakening,
bag-member_wf,
single-bag_wf,
bag-member-single,
bag_only_single_lemma,
true_wf,
single-valued-bag-single,
le_wf,
bag-member-size
\mforall{}[Info,A:Type]. \mforall{}[X:EClass(A)].
(Singlevalued(X) {}\mRightarrow{} (\mforall{}es:EO+(Info). \mforall{}e:E. \mforall{}v:A. (v \mmember{} X(e) \mLeftarrow{}{}\mRightarrow{} (\muparrow{}e \mmember{}\msubb{} X) \mwedge{} (v = X(e)))))
Date html generated:
2015_07_17-PM-00_41_24
Last ObjectModification:
2015_01_27-PM-11_11_15
Home
Index