Nuprl Lemma : dependent-choice

[T:ℕ ⟶ Type]. ∀[R:n:ℕ ⟶ T[n] ⟶ T[n 1] ⟶ ℙ].
  ((∀n:ℕ. ∀x:T[n].  ∃y:T[n 1]. R[n;x;y])
   (∀x0:T[0]. ∃f:n:ℕ ⟶ T[n]. (((f 0) x0 ∈ T[0]) ∧ (∀n:ℕR[n;f n;f (n 1)]))))


Proof




Definitions occuring in Statement :  nat: uall: [x:A]. B[x] prop: so_apply: x[s1;s2;s3] so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q apply: a function: x:A ⟶ B[x] add: m natural_number: $n universe: Type equal: t ∈ T
Definitions unfolded in proof :  cand: c∧ B assert: b bnot: ¬bb sq_type: SQType(T) bfalse: ff ifthenelse: if then else fi  btrue: tt it: unit: Unit bool: 𝔹 guard: {T} ge: i ≥  pi1: fst(t) so_apply: x[s1;s2;s3] true: True top: Top subtype_rel: A ⊆B subtract: m squash: T sq_stable: SqStable(P) uimplies: supposing a uiff: uiff(P;Q) rev_implies:  Q iff: ⇐⇒ Q or: P ∨ Q decidable: Dec(P) so_lambda: λ2x.t[x] prop: not: ¬A false: False less_than': less_than'(a;b) and: P ∧ Q le: A ≤ B nat: so_apply: x[s] member: t ∈ T exists: x:A. B[x] all: x:A. B[x] implies:  Q uall: [x:A]. B[x]
Lemmas referenced :  add-subtract-cancel primrec-wf2 set_wf primrec1_lemma le_weakening2 assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert le-add-cancel2 subtype_rel-equal assert_of_lt_int eqtt_to_assert bool_wf lt_int_wf primrec-unroll minus-minus less-iff-le not-ge-2 subtract_wf primrec0_lemma less_than_wf ge_wf less_than_irreflexivity less_than_transitivity1 nat_properties equal_wf subtype_rel_self le-add-cancel add-zero add_functionality_wrt_le add-commutes add-swap add-associates minus-one-mul-top zero-add minus-one-mul minus-add condition-implies-le sq_stable__le not-le-2 decidable__le exists_wf all_wf le_wf false_wf nat_wf
Rules used in proof :  productEquality instantiate equalityElimination axiomEquality intWeakElimination equalitySymmetry equalityTransitivity dependent_pairFormation universeEquality cumulativity functionEquality minusEquality intEquality voidEquality isect_memberEquality imageElimination baseClosed imageMemberEquality independent_isectElimination independent_functionElimination voidElimination unionElimination dependent_functionElimination rename setElimination addEquality because_Cache lambdaEquality isectElimination independent_pairFormation sqequalRule natural_numberEquality dependent_set_memberEquality extract_by_obid introduction hypothesisEquality functionExtensionality applyEquality productElimination sqequalHypSubstitution thin promote_hyp hypothesis cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[T:\mBbbN{}  {}\mrightarrow{}  Type].  \mforall{}[R:n:\mBbbN{}  {}\mrightarrow{}  T[n]  {}\mrightarrow{}  T[n  +  1]  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}n:\mBbbN{}.  \mforall{}x:T[n].    \mexists{}y:T[n  +  1].  R[n;x;y])
    {}\mRightarrow{}  (\mforall{}x0:T[0].  \mexists{}f:n:\mBbbN{}  {}\mrightarrow{}  T[n].  (((f  0)  =  x0)  \mwedge{}  (\mforall{}n:\mBbbN{}.  R[n;f  n;f  (n  +  1)]))))



Date html generated: 2018_07_25-PM-02_09_07
Last ObjectModification: 2018_07_25-PM-01_31_32

Theory : fun_1


Home Index