Nuprl Lemma : strong-continuity2-implies-uniform-continuity-int

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

Proof

Definitions occuring in Statement :  quotient: `x,y:A//B[x; y]` int_seg: `{i..j-}` nat: `ℕ` bool: `𝔹` 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]` member: `t ∈ T` implies: `P `` Q` nat: `ℕ` so_lambda: `λ2x.t[x]` prop: `ℙ` and: `P ∧ Q` so_apply: `x[s]` exists: `∃x:A. B[x]` uimplies: `b supposing a` isl: `isl(x)` sq_exists: `∃x:A [B[x]]` so_lambda: `λ2x y.t[x; y]` subtype_rel: `A ⊆r B` so_apply: `x[s1;s2]` quotient: `x,y:A//B[x; y]` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` guard: `{T}`
Lemmas referenced :  uniform-continuity-from-fan-ext istype-nat bool_wf istype-int strong-continuity2-no-inner-squash-cantor5 quotient_wf sq_exists_wf nat_wf int_seg_wf unit_wf2 all_wf exists_wf equal-wf-base-T isect_wf assert_wf istype-assert true_wf union_subtype_base int_subtype_base unit_subtype_base equiv_rel_true btrue_wf bfalse_wf quotient-member-eq subtype_rel_function int_seg_subtype_nat istype-false subtype_rel_self pi1_wf isl_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin intEquality dependent_functionElimination hypothesisEquality independent_functionElimination hypothesis Error :functionIsType,  Error :universeIsType,  rename pointwiseFunctionalityForEquality closedConclusion functionEquality natural_numberEquality setElimination unionEquality sqequalRule Error :lambdaEquality_alt,  productEquality because_Cache Error :inhabitedIsType,  unionElimination Error :equalityIstype,  equalityTransitivity equalitySymmetry Error :unionIsType,  Error :setIsType,  Error :productIsType,  applyEquality independent_isectElimination Error :inlEquality_alt,  sqequalBase Error :isectIsType,  isectEquality pertypeElimination promote_hyp productElimination independent_pairFormation Error :dependent_pairEquality_alt,  Error :dependent_set_memberEquality_alt

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

Date html generated: 2019_06_20-PM-02_52_56
Last ObjectModification: 2019_02_06-PM-05_39_36

Theory : continuity

Home Index