### Nuprl Lemma : decidable__exists_length

`∀[T:Type]. ∀[P:(T List) ⟶ ℙ].`
`  ((∀L:T List. Dec(P[L])) `` (∃k:ℕ. T ~ ℕk) `` (∀n:ℕ. Dec(∃L:T List. ((||L|| = n ∈ ℤ) ∧ P[L]))))`

Proof

Definitions occuring in Statement :  equipollent: `A ~ B` length: `||as||` list: `T List` int_seg: `{i..j-}` nat: `ℕ` 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` and: `P ∧ Q` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` nat: `ℕ` so_apply: `x[s]` equipollent: `A ~ B` biject: `Bij(A;B;f)` and: `P ∧ Q` surject: `Surj(A;B;f)` subtype_rel: `A ⊆r B` decidable: `Dec(P)` or: `P ∨ Q` guard: `{T}` pi1: `fst(t)` cand: `A c∧ B` not: `¬A` false: `False` inject: `Inj(A;B;f)`
Lemmas referenced :  nat_wf exists_wf equipollent_wf int_seg_wf all_wf list_wf decidable_wf equipollent-list decidable__exists_int_seg exp_wf2 equal_wf length_wf not_wf set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid hypothesis isectElimination sqequalRule lambdaEquality cumulativity hypothesisEquality natural_numberEquality setElimination rename applyEquality functionExtensionality functionEquality universeEquality dependent_functionElimination independent_functionElimination promote_hyp instantiate because_Cache setEquality intEquality unionElimination inlFormation productEquality inrFormation dependent_set_memberEquality dependent_pairFormation equalityTransitivity equalitySymmetry independent_pairFormation voidElimination addLevel hyp_replacement levelHypothesis

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}L:T  List.  Dec(P[L]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  Dec(\mexists{}L:T  List.  ((||L||  =  n)  \mwedge{}  P[L]))))

Date html generated: 2017_04_17-AM-09_36_04
Last ObjectModification: 2017_02_27-PM-05_34_11

Theory : equipollence!!cardinality!

Home Index