### Nuprl Lemma : decidable-exists-finite-type

`∀[T:Type]. (finite-type(T) `` (∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) `` Dec(∃t:T. P[t]))))`

Proof

Definitions occuring in Statement :  finite-type: `finite-type(T)` 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]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` finite-type: `finite-type(T)` exists: `∃x:A. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` decidable: `Dec(P)` or: `P ∨ Q` prop: `ℙ` not: `¬A` false: `False` surject: `Surj(A;B;f)` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  decidable__exists_int_seg int_seg_wf all_wf decidable_wf finite-type_wf not_wf exists_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution productElimination thin cut instantiate lemma_by_obid dependent_functionElimination natural_numberEquality setElimination rename hypothesisEquality isectElimination sqequalRule lambdaEquality applyEquality hypothesis independent_functionElimination unionElimination functionEquality cumulativity universeEquality inlFormation dependent_pairFormation inrFormation introduction voidElimination because_Cache equalityTransitivity equalitySymmetry independent_isectElimination

Latex:
\mforall{}[T:Type].  (finite-type(T)  {}\mRightarrow{}  (\mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}t:T.  Dec(P[t]))  {}\mRightarrow{}  Dec(\mexists{}t:T.  P[t]))))

Date html generated: 2016_05_14-PM-01_51_22
Last ObjectModification: 2015_12_26-PM-05_37_35

Theory : list_1

Home Index