Nuprl Lemma : es-le_antisymmetry

∀[es:EO]. ∀[e,e':E].  (e = e' ∈ E) supposing (e' ≤loc e  and e ≤loc e' )


Proof



Definitions occuring in Statement :  es-le: e ≤loc e' ,  es-E: E,  event_ordering: EO,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  equal: s = t ∈ T
Latex:
\mforall{}[es:EO].  \mforall{}[e,e':E].    (e  =  e')  supposing  (e'  \mleq{}loc  e    and  e  \mleq{}loc  e'  )


Date html generated: 2016_05_16-AM-09_23_09
Last ObjectModification: 2015_12_28-PM-09_51_29

Theory : new!event-ordering


Home Index