Nuprl Lemma : decidable__exists-es-p-le-pred

es:EO. ∀[P:E ─→ ℙ]. ∀e:E. ((∀e:E. Dec(P e))  Dec(∃a:E. (es-p-le-pred(es;P) a)))


Proof




Definitions occuring in Statement :  es-p-le-pred: es-p-le-pred(es;P) es-E: E event_ordering: EO decidable: Dec(P) uall: [x:A]. B[x] prop: all: x:A. B[x] exists: x:A. B[x] implies:  Q apply: a function: x:A ─→ B[x]
Lemmas :  all_wf es-E_wf decidable_wf event_ordering_wf decidable__existse-le Id_wf es-loc_wf alle-le_wf es-locl_wf not_wf equal_wf decidable__implies decidable__es-locl decidable__not decidable__cand decidable__alle-le
\mforall{}es:EO.  \mforall{}[P:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}e:E.  ((\mforall{}e:E.  Dec(P  e))  {}\mRightarrow{}  Dec(\mexists{}a:E.  (es-p-le-pred(es;P)  e  a)))



Date html generated: 2015_07_17-AM-08_58_55
Last ObjectModification: 2015_01_27-PM-01_03_46

Home Index