Nuprl Lemma : simple-dependent-choice

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


Proof




Definitions occuring in Statement :  nat: uall: [x:A]. B[x] prop: so_apply: x[s1;s2] 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 :  assert: b bnot: ¬bb sq_type: SQType(T) guard: {T} btrue: tt it: unit: Unit bool: 𝔹 bfalse: ff ifthenelse: if then else fi  eq_int: (i =z j) compose: g pi1: fst(t) so_apply: x[s] 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_apply: x[s1;s2] so_lambda: λ2x.t[x] not: ¬A false: False less_than': less_than'(a;b) le: A ≤ B nat: prop: primrec: primrec(n;b;c) fun_exp: f^n cand: c∧ B and: P ∧ Q member: t ∈ T exists: x:A. B[x] all: x:A. B[x] implies:  Q uall: [x:A]. B[x]
Lemmas referenced :  le_weakening2 primrec-wf2 less_than_wf set_wf minus-minus subtract_wf add-subtract-cancel neg_assert_of_eq_int assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert le_antisymmetry_iff assert_of_eq_int eqtt_to_assert bool_wf eq_int_wf less-iff-le fun_exp_unroll exists_wf 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 all_wf le_wf false_wf equal_wf nat_wf fun_exp_wf
Rules used in proof :  instantiate equalityElimination equalitySymmetry equalityTransitivity universeEquality functionEquality minusEquality intEquality voidEquality isect_memberEquality imageElimination baseClosed imageMemberEquality independent_isectElimination independent_functionElimination voidElimination unionElimination dependent_functionElimination rename setElimination addEquality because_Cache natural_numberEquality dependent_set_memberEquality functionExtensionality cumulativity productEquality independent_pairFormation sqequalRule hypothesisEquality isectElimination extract_by_obid introduction applyEquality lambdaEquality dependent_pairFormation productElimination sqequalHypSubstitution thin promote_hyp hypothesis cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

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



Date html generated: 2018_07_25-PM-02_09_04
Last ObjectModification: 2018_07_25-PM-01_14_39

Theory : fun_1


Home Index