### Nuprl Lemma : cantor-to-general-cantor

`∀B:ℕ ⟶ ℕ+`
`  ∃f:(ℕ ⟶ 𝔹) ⟶ n:ℕ ⟶ ℕB[n]`
`   (Surj(ℕ ⟶ 𝔹;n:ℕ ⟶ ℕB[n];f)`
`   ∧ (∀k:ℕ. ∃j:ℕ. ∀p,q:ℕ ⟶ 𝔹.  ((p = q ∈ (ℕj ⟶ 𝔹)) `` ((f p) = (f q) ∈ (n:ℕk ⟶ ℕB[n])))))`

Proof

Definitions occuring in Statement :  surject: `Surj(A;B;f)` int_seg: `{i..j-}` nat_plus: `ℕ+` nat: `ℕ` bool: `𝔹` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  inject: `Inj(A;B;f)` compose: `f o g` surject: `Surj(A;B;f)` biject: `Bij(A;B;f)` equipollent: `A ~ B` pi1: `fst(t)` rev_uimplies: `rev_uimplies(P;Q)` subtract: `n - m` so_apply: `x[s]` so_lambda: `λ2x.t[x]` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` assert: `↑b` bnot: `¬bb` sq_type: `SQType(T)` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` cand: `A c∧ B` lelt: `i ≤ j < k` int_seg: `{i..j-}` le: `A ≤ B` guard: `{T}` false: `False` prop: `ℙ` top: `Top` satisfiable_int_formula: `satisfiable_int_formula(fmla)` implies: `P `` Q` not: `¬A` uimplies: `b supposing a` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` nat: `ℕ` subtype_rel: `A ⊆r B` and: `P ∧ Q` true: `True` less_than': `less_than'(a;b)` squash: `↓T` less_than: `a < b` uall: `∀[x:A]. B[x]` nat_plus: `ℕ+` member: `t ∈ T` exists: `∃x:A. B[x]` all: `∀x:A. B[x]`
Lemmas referenced :  int_seg_subtype equal_wf subtype_rel_dep_function int_seg_subtype_nat subtype_rel_function istype-universe equipollent_wf equipollent-int_seg-shift decidable__equal_int_seg compose_wf surject_wf lelt_wf ifthenelse_wf equipollent_transitivity equipollent-two indep-function_functionality_wrt_equipollent equipollent-exp equal-wf-base primrec-wf2 le_weakening2 le_weakening le_functionality imax_ub exp_functionality_wrt_le_1 imax_nat add-zero zero-mul add-mul-special add-swap minus-one-mul int_term_value_subtract_lemma itermSubtract_wf subtract_wf primrec-wf-nat-plus general_add_assoc iff_weakening_equal subtype_rel_self true_wf squash_wf int_subtype_base le_wf set_subtype_base istype-false decidable__equal_int add-subtract-cancel less_than_wf assert_wf iff_weakening_uiff assert-bnot bool_subtype_base bool_wf subtype_base_sq bool_cases_sqequal eqff_to_assert assert_of_lt_int eqtt_to_assert lt_int_wf primrec-unroll primrec0_lemma int_seg_wf false_wf int_term_value_add_lemma itermAdd_wf add_nat_wf int_formula_prop_le_lemma intformle_wf decidable__le int_seg_properties nat_wf primrec_wf nat_plus_subtype_nat exp_wf2 istype-le log-property istype-nat int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_and_lemma intformeq_wf itermVar_wf intformand_wf nat_plus_properties int_formula_prop_wf int_term_value_constant_lemma int_formula_prop_less_lemma istype-void int_formula_prop_not_lemma istype-int itermConstant_wf intformless_wf intformnot_wf full-omega-unsat decidable__lt nat_properties nat_plus_wf imax_nat_plus istype-less_than log_wf imax_wf
Rules used in proof :  functionExtensionality productEquality setIsType baseApply inlFormation_alt functionEquality universeEquality sqequalBase productIsType intEquality cumulativity instantiate equalityElimination promote_hyp pointwiseFunctionality imageElimination addEquality productElimination functionIsType equalityIstype int_eqEquality applyLambdaEquality equalitySymmetry equalityTransitivity inhabitedIsType voidElimination isect_memberEquality_alt independent_functionElimination approximateComputation independent_isectElimination unionElimination dependent_functionElimination universeIsType rename setElimination closedConclusion applyEquality because_Cache hypothesis baseClosed hypothesisEquality imageMemberEquality independent_pairFormation sqequalRule natural_numberEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction dependent_set_memberEquality_alt lambdaEquality_alt dependent_pairFormation_alt cut lambdaFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
\mexists{}f:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n]
(Surj(\mBbbN{}  {}\mrightarrow{}  \mBbbB{};n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n];f)  \mwedge{}  (\mforall{}k:\mBbbN{}.  \mexists{}j:\mBbbN{}.  \mforall{}p,q:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((p  =  q)  {}\mRightarrow{}  ((f  p)  =  (f  q)))))

Date html generated: 2019_10_15-AM-10_26_32
Last ObjectModification: 2019_10_03-PM-06_54_31

Theory : continuity

Home Index