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) e 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: P ⇒ Q,
apply: f 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