Nuprl Lemma : cantor-to-int-bounded

`∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. ∃B:ℕ. ∀f:ℕ ⟶ 𝔹. (|F f| ≤ B)`

Proof

Definitions occuring in Statement :  absval: `|i|` nat: `ℕ` bool: `𝔹` le: `A ≤ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` exists: `∃x:A. B[x]` uall: `∀[x:A]. B[x]` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` l_member: `(x ∈ l)` cand: `A c∧ B` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` squash: `↓T` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` prop: `ℙ` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` int_seg: `{i..j-}` lelt: `i ≤ j < k` bfalse: `ff` subtype_rel: `A ⊆r B` listp: `A List+` rev_implies: `P `` Q` l_exists: `(∃x∈L. P[x])` true: `True` guard: `{T}` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` le: `A ≤ B` less_than': `less_than'(a;b)`
Lemmas referenced :  cantor-to-int-uniform-continuity istype-nat bool_wf istype-int finite-function int_seg_wf nsub_finite finite-bool finite-iff-listable bfalse_wf nat_properties decidable__lt length_wf full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformle_wf int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf istype-le absval_wf lt_int_wf eqtt_to_assert assert_of_lt_int decidable__le istype-less_than imax-list-nat map-length map_wf nat_wf imax-list-ub length-map select-map subtype_rel_list top_wf le_weakening squash_wf true_wf equal_wf istype-universe subtype_rel_self iff_weakening_equal eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf int_seg_properties select_wf subtype_rel_function int_seg_subtype_nat istype-false le_wf ifthenelse_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality productElimination functionIsType universeIsType isectElimination natural_numberEquality setElimination rename because_Cache sqequalRule lambdaEquality_alt independent_functionElimination functionEquality unionElimination imageElimination independent_isectElimination approximateComputation dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation applyEquality inhabitedIsType equalityElimination dependent_set_memberEquality_alt productIsType equalityIstype equalityTransitivity equalitySymmetry closedConclusion intEquality functionExtensionality functionExtensionality_alt instantiate universeEquality imageMemberEquality baseClosed promote_hyp cumulativity hyp_replacement

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbZ{}.  \mexists{}B:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (|F  f|  \mleq{}  B)

Date html generated: 2019_10_15-AM-10_26_19
Last ObjectModification: 2019_06_26-PM-02_45_48

Theory : continuity

Home Index