Nuprl Lemma : dec-exists-int-seg
∀a,b:ℤ. ∀[F:{a..b-} ⟶ ℙ]. ((∀k:{a..b-}. Dec(F[k])) ⇒ Dec(∃k:{a..b-}. F[k]))
Proof
Definitions occuring in Statement :
int_seg: {i..j-},
decidable: Dec(P),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
int: ℤ
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ
Lemmas referenced :
decidable_wf,
all_wf,
int_seg_wf,
decidable__exists_int_seg
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
thin,
instantiate,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
hypothesisEquality,
isectElimination,
sqequalRule,
lambdaEquality,
applyEquality,
hypothesis,
independent_functionElimination,
functionEquality,
cumulativity,
universeEquality,
intEquality
Latex:
\mforall{}a,b:\mBbbZ{}. \mforall{}[F:\{a..b\msupminus{}\} {}\mrightarrow{} \mBbbP{}]. ((\mforall{}k:\{a..b\msupminus{}\}. Dec(F[k])) {}\mRightarrow{} Dec(\mexists{}k:\{a..b\msupminus{}\}. F[k]))
Date html generated:
2016_05_14-PM-09_56_16
Last ObjectModification:
2016_01_16-PM-05_37_41
Theory : continuity
Home
Index