Nuprl Lemma : general-cantor-to-int-uniform-continuity

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

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat_plus: `ℕ+` nat: `ℕ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` gt: `i > j` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` assert: `↑b` bnot: `¬bb` sq_type: `SQType(T)` bfalse: `ff` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` cand: `A c∧ B` guard: `{T}` istype: `istype(T)` top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` squash: `↓T` less_than: `a < b` lelt: `i ≤ j < k` int_seg: `{i..j-}` not: `¬A` false: `False` less_than': `less_than'(a;b)` and: `P ∧ Q` le: `A ≤ B` uimplies: `b supposing a` nat: `ℕ` prop: `ℙ` implies: `P `` Q` so_lambda: `λ2x.t[x]` nat_plus: `ℕ+` subtype_rel: `A ⊆r B` so_apply: `x[s]` uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]`
Lemmas referenced :  le_witness int_formula_prop_eq_lemma intformeq_wf prop-truncation-implies mu-dec-property it_wf unit_wf2 mu-dec_wf change-equality-type respects-equality-trivial not-gt-2 respects-equality-function subtype_rel_transitivity istype-universe true_wf squash_wf decidable__equal_int decidable__not decidable__and2 nat_plus_properties 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 not_wf decidable-exists-finite istype-less_than int_formula_prop_less_lemma intformless_wf decidable__equal_int_seg lelt_wf set_subtype_base le_weakening2 int_seg_subtype decidable__all_int_seg nat_plus_subtype_nat nsub_finite finite-function decidable__lt le_wf int_subtype_base equal-wf-base 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 nat_properties int_seg_properties subtype_rel_dep_function istype-false int_seg_subtype_nat equal_wf all_wf nat_wf exists_wf implies-quotient-true istype-int nat_plus_wf int_seg_wf istype-nat general-cantor-to-int-uniform-continuity-half-squashed
Rules used in proof :  independent_pairEquality dependent_pairEquality_alt baseClosed imageMemberEquality universeEquality hyp_replacement functionExtensionality_alt cumulativity promote_hyp equalityElimination applyLambdaEquality equalityTransitivity inrFormation_alt functionExtensionality inlFormation_alt instantiate equalitySymmetry sqequalBase equalityIstype productIsType productEquality intEquality voidElimination isect_memberEquality_alt int_eqEquality dependent_pairFormation_alt independent_functionElimination approximateComputation unionElimination imageElimination dependent_set_memberEquality_alt productElimination inhabitedIsType independent_pairFormation independent_isectElimination closedConclusion because_Cache functionEquality sqequalRule rename setElimination lambdaEquality_alt applyEquality natural_numberEquality isectElimination universeIsType functionIsType hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution hypothesis lambdaFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution extract_by_obid introduction cut

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

Date html generated: 2019_10_15-AM-10_26_13
Last ObjectModification: 2019_10_08-PM-05_31_18

Theory : continuity

Home Index