Nuprl Lemma : es-fset-loc-iff
∀es:EO. ∀s:fset(E). ∀i:Id.  (i ∈ locs(s) 
⇐⇒ ∃e:E. ((loc(e) = i ∈ Id) ∧ e ∈ s))
Proof
Definitions occuring in Statement : 
es-fset-loc: i ∈ locs(s)
, 
es-eq: es-eq(es)
, 
es-loc: loc(e)
, 
es-E: E
, 
event_ordering: EO
, 
Id: Id
, 
fset-member: a ∈ s
, 
fset: fset(T)
, 
all: ∀x:A. B[x]
, 
exists: ∃x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
and: P ∧ Q
, 
equal: s = t ∈ T
Lemmas : 
es-fset-at-property, 
es-fset-at_wf, 
list_wf, 
not_wf, 
assert_wf, 
null_wf3, 
subtype_rel_list, 
top_wf, 
exists_wf, 
es-loc_wf, 
fset-member_wf, 
es-eq_wf, 
all_wf, 
iff_wf, 
l_member_wf, 
no_repeats_wf, 
sorted-by_wf, 
es-le_wf, 
Id_wf, 
fset_wf, 
es-E_wf, 
event_ordering_wf, 
list-cases, 
product_subtype_list, 
null_nil_lemma, 
cons_member, 
btrue_wf, 
member-implies-null-eq-bfalse, 
btrue_neq_bfalse, 
null_cons_lemma, 
false_wf
\mforall{}es:EO.  \mforall{}s:fset(E).  \mforall{}i:Id.    (i  \mmember{}  locs(s)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e:E.  ((loc(e)  =  i)  \mwedge{}  e  \mmember{}  s))
Date html generated:
2015_07_17-AM-09_01_05
Last ObjectModification:
2015_01_27-PM-00_55_38
Home
Index