Nuprl Lemma : decidable__l_all-better-extract
∀[A:Type]. ∀L:A List. ∀[F:{a:A| (a ∈ L)} ⟶ ℙ]. ((∀k:{a:A| (a ∈ L)} . Dec(F[k])) ⇒ Dec((∀k∈L.F[k])))
Proof
Definitions occuring in Statement :
l_all: (∀x∈L.P[x]),
l_member: (x ∈ l),
list: T List,
decidable: Dec(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
universe: Type
Lemmas referenced :
decidable__l_all
Rules used in proof :
cut,
lemma_by_obid,
hypothesis
Latex:
\mforall{}[A:Type]. \mforall{}L:A List. \mforall{}[F:\{a:A| (a \mmember{} L)\} {}\mrightarrow{} \mBbbP{}]. ((\mforall{}k:\{a:A| (a \mmember{} L)\} . Dec(F[k])) {}\mRightarrow{} Dec((\mforall{}k\mmember{}L.F[k])\000C))
Date html generated:
2016_05_15-PM-04_20_13
Last ObjectModification:
2015_12_27-PM-02_55_14
Theory : general
Home
Index