### Nuprl Lemma : fun2listCantor

`∀n:ℕ. ∀f:ℕn ⟶ 𝔹.  ∃l:𝔹 List. ((||l|| = n ∈ ℤ) ∧ (f = (λx.l[x]) ∈ (ℕn ⟶ 𝔹)))`

Proof

Definitions occuring in Statement :  select: `L[n]` length: `||as||` list: `T List` int_seg: `{i..j-}` nat: `ℕ` bool: `𝔹` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` subtype_rel: `A ⊆r B` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` decidable: `Dec(P)` or: `P ∨ Q` ge: `i ≥ j ` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` cand: `A c∧ B` le: `A ≤ B` less_than': `less_than'(a;b)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` true: `True` label: `...\$L... t` squash: `↓T`
Lemmas referenced :  int_seg_wf int_seg_properties full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf bool_wf subtract_wf list_wf length_wf_nat set_subtype_base le_wf int_subtype_base select_wf decidable__le intformnot_wf int_formula_prop_not_lemma decidable__lt itermSubtract_wf intformeq_wf int_term_value_subtract_lemma int_formula_prop_eq_lemma istype-less_than primrec-wf2 all_wf exists_wf equal-wf-base equal_wf nat_properties istype-nat nil_wf length_of_nil_lemma stuck-spread istype-base subtype_rel_function int_seg_subtype istype-false not-le-2 condition-implies-le add-associates minus-add minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul add-zero add-commutes le-add-cancel2 subtype_rel_self append_wf cons_wf istype-le length-append length_of_cons_lemma decidable__equal_int itermAdd_wf int_term_value_add_lemma length_wf squash_wf true_wf istype-universe less_than_wf iff_weakening_equal select_append_back select-cons-hd select_append_front
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut thin Error :functionIsType,  Error :universeIsType,  introduction extract_by_obid sqequalHypSubstitution isectElimination natural_numberEquality hypothesis hypothesisEquality setElimination rename productElimination independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  int_eqEquality dependent_functionElimination Error :isect_memberEquality_alt,  voidElimination sqequalRule independent_pairFormation Error :productIsType,  Error :equalityIstype,  Error :inhabitedIsType,  applyEquality intEquality closedConclusion because_Cache baseApply baseClosed sqequalBase equalitySymmetry equalityTransitivity unionElimination Error :setIsType,  functionEquality productEquality Error :functionExtensionality_alt,  addEquality minusEquality multiplyEquality Error :dependent_set_memberEquality_alt,  functionExtensionality imageElimination instantiate universeEquality imageMemberEquality Error :equalityIsType1

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    \mexists{}l:\mBbbB{}  List.  ((||l||  =  n)  \mwedge{}  (f  =  (\mlambda{}x.l[x])))

Date html generated: 2019_06_20-PM-02_53_05
Last ObjectModification: 2018_11_22-AM-09_59_24

Theory : continuity

Home Index