Nuprl Lemma : seq-cont-nat

F:(ℕ ⟶ ℕ) ⟶ ℕseq-cont(ℕ;F)


Proof




Definitions occuring in Statement :  seq-cont: seq-cont(T;F) nat: all: x:A. B[x] function: x:A ⟶ B[x]
Definitions unfolded in proof :  guard: {T} exists: x:A. B[x] not: ¬A false: False less_than': less_than'(a;b) le: A ≤ B uimplies: supposing a so_apply: x[s] subtype_rel: A ⊆B and: P ∧ Q prop: so_lambda: λ2x.t[x] nat: uall: [x:A]. B[x] member: t ∈ T implies:  Q seq-cont: seq-cont(T;F) all: x:A. B[x] true: True btrue: tt ifthenelse: if then else fi  assert: b sq_type: SQType(T) isl: isl(x) rev_implies:  Q iff: ⇐⇒ Q squash: T cand: c∧ B top: Top satisfiable_int_formula: satisfiable_int_formula(fmla) or: P ∨ Q decidable: Dec(P) ge: i ≥  int_upper: {i...} outl: outl(x)
Lemmas referenced :  int_upper_subtype_nat int_upper_wf isl_wf assert_wf isect_wf subtype_rel_self false_wf int_seg_subtype_nat nat_wf subtype_rel_dep_function equal_wf all_wf unit_wf2 int_seg_wf exists_wf implies-quotient-true strong-continuity2-no-inner-squash bool_subtype_base bool_wf subtype_base_sq btrue_wf and_wf iff_weakening_equal true_wf squash_wf int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma itermConstant_wf intformle_wf intformand_wf decidable__le le_wf int_formula_prop_wf int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermVar_wf intformeq_wf intformnot_wf full-omega-unsat btrue_neq_bfalse int_subtype_base subtype_rel-equal bfalse_wf decidable__equal_int nat_properties int_upper_properties
Rules used in proof :  productElimination independent_functionElimination inlEquality independent_pairFormation independent_isectElimination functionExtensionality applyEquality productEquality lambdaEquality sqequalRule unionEquality hypothesis rename setElimination natural_numberEquality because_Cache functionEquality isectElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution dependent_pairFormation cumulativity instantiate applyLambdaEquality equalitySymmetry equalityTransitivity dependent_set_memberEquality baseClosed imageMemberEquality universeEquality imageElimination voidEquality isect_memberEquality int_eqEquality approximateComputation voidElimination intEquality promote_hyp unionElimination

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}.  seq-cont(\mBbbN{};F)



Date html generated: 2017_09_29-PM-06_05_48
Last ObjectModification: 2017_07_19-AM-11_24_59

Theory : continuity


Home Index