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

`∀B:ℕ ⟶ ℕ+. ∀F:(n:ℕ ⟶ ℕB[n]) ⟶ ℤ.  ∃bnd:ℕ. ∀f:n:ℕ ⟶ ℕB[n]. (|F f| ≤ bnd)`

Proof

Definitions occuring in Statement :  absval: `|i|` int_seg: `{i..j-}` nat_plus: `ℕ+` nat: `ℕ` so_apply: `x[s]` le: `A ≤ B` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  implies: `P `` Q` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` guard: `{T}` uimplies: `b supposing a` true: `True` prop: `ℙ` squash: `↓T` surject: `Surj(A;B;f)` nat_plus: `ℕ+` nat: `ℕ` compose: `f o g` subtype_rel: `A ⊆r B` so_apply: `x[s]` uall: `∀[x:A]. B[x]` and: `P ∧ Q` exists: `∃x:A. B[x]` member: `t ∈ T` all: `∀x:A. B[x]`
Lemmas referenced :  iff_weakening_equal subtype_rel_self true_wf squash_wf le_wf istype-int nat_plus_wf istype-nat absval_wf istype-le int_seg_wf bool_wf nat_wf compose_wf cantor-to-int-bounded cantor-to-general-cantor
Rules used in proof :  independent_functionElimination independent_isectElimination universeEquality instantiate baseClosed imageMemberEquality inhabitedIsType equalitySymmetry equalityTransitivity imageElimination universeIsType rename setElimination lambdaEquality_alt functionIsType dependent_pairFormation_alt intEquality sqequalRule because_Cache applyEquality natural_numberEquality hypothesis functionEquality isectElimination productElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}.  \mforall{}F:(n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n])  {}\mrightarrow{}  \mBbbZ{}.    \mexists{}bnd:\mBbbN{}.  \mforall{}f:n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n].  (|F  f|  \mleq{}  bnd)

Date html generated: 2019_10_15-AM-10_26_35
Last ObjectModification: 2019_10_03-PM-06_59_43

Theory : continuity

Home Index