### Nuprl Lemma : twkl!-implies-dfan

`∀T:Type. ((∃k:ℕ. T ~ ℕk) `` WKL!(T) `` Fan_d(T))`

Proof

Definitions occuring in Statement :  twkl!: `WKL!(T)` dfan: `Fan_d(T)` equipollent: `A ~ B` int_seg: `{i..j-}` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` dfan: `Fan_d(T)` dbar: `dbar(T;X)` and: `P ∧ Q` tbar: `tbar(T;X)` dec-predicate: `Decidable(X)` ubar: `ubar(T;X)` member: `t ∈ T` uall: `∀[x:A]. B[x]` decidable: `Dec(P)` or: `P ∨ Q` prop: `ℙ` so_lambda: `λ2x.t[x]` nat: `ℕ` so_apply: `x[s]` exists: `∃x:A. B[x]` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` int_seg: `{i..j-}` lelt: `i ≤ j < k` less_than: `a < b` squash: `↓T` true: `True` upto: `upto(n)` from-upto: `[n, m)` ifthenelse: `if b then t else f fi ` lt_int: `i <z j` bfalse: `ff` top: `Top` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` pi1: `fst(t)` compose: `f o g` cand: `A c∧ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` sq_type: `SQType(T)` equipollent: `A ~ B` biject: `Bij(A;B;f)` surject: `Surj(A;B;f)` twkl!: `WKL!(T)` down-closed: `down-closed(T;X)` R-closed: `R-closed(T;x.X[x];a,b.R[a; b])` upwd-closure: `upwd-closure(T;A)` let: let unbounded-list-predicate: `Unbounded(A)` label: `...\$L... t` uiff: `uiff(P;Q)` tree-big: `tree-big(T;A;n)` eff-unique-path: `eff-unique-path(T;A)` sq_exists: `∃x:{A| B[x]}` is-path: `is-path(A;f)` sq_stable: `SqStable(P)` compat: `l1 || l2`
Lemmas referenced :  nil_wf tree-big-monotone dbar_wf list_wf twkl!_wf exists_wf nat_wf equipollent_wf int_seg_wf false_wf le_wf lelt_wf map_nil_lemma map_wf subtype_rel_dep_function int_seg_subtype_nat upto_wf all_wf tree-big-least not-tree-big set_wf tree-big_wf upwd-closure_wf not_wf int_seg_properties nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf equal_wf decidable__tree-big decidable__upwd-closure length_wf compose_wf less_than_wf squash_wf true_wf iff_weakening_equal decidable__lt intformless_wf int_formula_prop_less_lemma subtype_base_sq int_subtype_base add_nat_wf intformeq_wf int_formula_prop_eq_lemma decidable__equal_int non_neg_length equipollent-zero decidable__equal_equipollent length_wf_nat let_wf append_wf subtract_wf iseg_wf iseg_transitivity iseg_append_iff length-append map-length length_upto le_weakening2 length_append subtype_rel_list top_wf itermSubtract_wf int_term_value_subtract_lemma list_extensionality length-map select-map iseg_select and_wf decidable__exists_length decidable__not not_over_exists down-closed_wf unbounded-list-predicate_wf decidable__implies decidable__and2 decidable__equal_list imax_ub imax_wf iseg-map int_seg_subtype upto_iseg select_wf select-upto sq_stable_from_decidable decidable__exists_int_seg iseg_weakening iseg_length common_iseg_compat iseg_same_length
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin rename cut hypothesis dependent_functionElimination introduction extract_by_obid isectElimination cumulativity hypothesisEquality unionElimination functionExtensionality applyEquality functionEquality universeEquality sqequalRule lambdaEquality natural_numberEquality setElimination dependent_pairFormation dependent_set_memberEquality independent_pairFormation because_Cache imageMemberEquality baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination independent_functionElimination promote_hyp setEquality productEquality addEquality int_eqEquality intEquality computeAll equalityTransitivity equalitySymmetry applyLambdaEquality imageElimination instantiate addLevel levelHypothesis hyp_replacement inlFormation inrFormation

Latex:
\mforall{}T:Type.  ((\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)  {}\mRightarrow{}  WKL!(T)  {}\mRightarrow{}  Fan\_d(T))

Date html generated: 2017_04_17-AM-09_38_44
Last ObjectModification: 2017_02_27-PM-05_43_56

Theory : fan-theorem

Home Index