Nuprl Lemma : es-first-at-unique

[es:EO]. ∀[i:Id]. ∀[P:{e:E| loc(e) i ∈ Id}  ─→ ℙ]. ∀[e1,e2:E].
  (e1 e2 ∈ E) supposing (e2 is first@ s.t.  e.P[e] and e1 is first@ s.t.  e.P[e])


Definitions occuring in Statement :  es-first-at: is first@ s.t.  e.P[e] es-loc: loc(e) es-E: E event_ordering: EO Id: Id uimplies: supposing a uall: [x:A]. B[x] prop: so_apply: x[s] set: {x:A| B[x]}  function: x:A ─→ B[x] equal: t ∈ T
Lemmas :  es-locl-total es-first-at_wf Id_wf es-loc_wf es-E_wf event_ordering_wf
\mforall{}[es:EO].  \mforall{}[i:Id].  \mforall{}[P:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}].  \mforall{}[e1,e2:E].
    (e1  =  e2)  supposing  (e2  is  first@  i  s.t.    e.P[e]  and  e1  is  first@  i  s.t.    e.P[e])

Date html generated: 2015_07_17-AM-08_50_15
Last ObjectModification: 2015_01_27-PM-02_26_00

Home Index