### Nuprl Lemma : general-cantor-to-int-uniform-continuity-half-squashed

`∀B:ℕ ⟶ ℕ+. ∀F:(i:ℕ ⟶ ℕB[i]) ⟶ ℤ.  ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) `` ((F f) = (F g) ∈ ℤ)))`

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` int_seg: `{i..j-}` nat_plus: `ℕ+` nat: `ℕ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` true: `True` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` member: `t ∈ T` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` implies: `P `` Q` nat_plus: `ℕ+` guard: `{T}` prop: `ℙ` top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` nat: `ℕ` not: `¬A` false: `False` less_than': `less_than'(a;b)` le: `A ≤ B` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` listp: `A List+` sq_exists: `∃x:A [B[x]]` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` squash: `↓T` less_than: `a < b` l_exists: `(∃x∈L. P[x])` istype: `istype(T)` isl: `isl(x)` nequal: `a ≠ b ∈ T ` assert: `↑b` bnot: `¬bb` sq_type: `SQType(T)` uiff: `uiff(P;Q)` bfalse: `ff` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹`
Lemmas referenced :  general-uniform-continuity-from-fan-ext int_seg_wf istype-nat nat_plus_wf istype-int istype-less_than int_formula_prop_less_lemma intformless_wf nat_plus_properties istype-le int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma istype-void int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf full-omega-unsat decidable__le decidable__lt nat_properties istype-false le_wf sq_exists_wf nat_wf trivial-quotient-true length_wf upto_wf map_wf length_upto map-length imax-list-nat int_seg_properties imax-list-ub select_wf nat_plus_subtype_nat select-upto top_wf subtype_rel_list select-map strong-continuity2-half-squash-surject-biject-ext countable-nsub-family biject-int-nat int_subtype_base set_subtype_base zero-le-nat subtype_rel_dep_function istype-assert unit_subtype_base union_subtype_base subtype_rel_self int_seg_subtype_nat subtype_rel_function bfalse_wf btrue_wf assert_wf isect_wf equal-wf-base-T all_wf unit_wf2 exists_wf implies-quotient-true2 neg_assert_of_eq_int assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert eq_int_wf int_formula_prop_eq_lemma intformeq_wf bool_wf assert_of_eq_int eqtt_to_assert
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality_alt natural_numberEquality applyEquality hypothesisEquality hypothesis because_Cache independent_isectElimination independent_functionElimination intEquality dependent_functionElimination functionIsType universeIsType setElimination rename productIsType applyLambdaEquality equalitySymmetry equalityTransitivity voidElimination isect_memberEquality_alt int_eqEquality dependent_pairFormation_alt approximateComputation unionElimination independent_pairFormation dependent_set_memberEquality_alt equalityIstype inhabitedIsType functionEquality dependent_set_memberFormation_alt functionExtensionality imageElimination productElimination productEquality sqequalBase isectIsType unionIsType spreadEquality inlEquality_alt unionEquality closedConclusion instantiate promote_hyp equalityElimination isect_memberFormation_alt cumulativity dependent_pairEquality_alt

Latex:
\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}.  \mforall{}F:(i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i])  {}\mrightarrow{}  \mBbbZ{}.    \00D9(\mexists{}n:\mBbbN{}.  \mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))

Date html generated: 2020_05_19-PM-10_04_56
Last ObjectModification: 2019_11_22-AM-10_51_12

Theory : continuity

Home Index