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

`∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. ∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) `` ((F f) = (F g) ∈ ℤ))`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat: `ℕ` bool: `𝔹` 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 :  member: `t ∈ T` subtract: `n - m` ifthenelse: `if b then t else f fi ` ext2Cantor: `ext2Cantor(n;f;d)` lt_int: `i <z j` it: `⋅` bfalse: `ff` btrue: `tt` strong-continuity2-implies-uniform-continuity2-int uniform-continuity-pi-pi-prop2 decidable__equal_int prop-truncation-implies strong-continuity2-implies-uniform-continuity-int-ext uniform-continuity-pi-dec decidable__int_equal sq_stable__all sq_stable__le any: `any x` decidable_functionality uniform-continuity-pi2-dec-ext iff_weakening_equal iff_preserves_decidability uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  strong-continuity2-implies-uniform-continuity2-int lifting-strict-spread istype-void strict4-spread lifting-strict-callbyvalue lifting-strict-decide strict4-decide lifting-strict-int_eq lifting-strict-less uniform-continuity-pi-pi-prop2 decidable__equal_int prop-truncation-implies strong-continuity2-implies-uniform-continuity-int-ext uniform-continuity-pi-dec decidable__int_equal sq_stable__all sq_stable__le decidable_functionality uniform-continuity-pi2-dec-ext iff_weakening_equal iff_preserves_decidability
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed Error :isect_memberEquality_alt,  voidElimination independent_isectElimination

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbZ{}.  \mexists{}n:\mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))

Date html generated: 2019_06_20-PM-02_53_31
Last ObjectModification: 2019_03_12-PM-05_57_02

Theory : continuity

Home Index