Nuprl Lemma : init0-baire-eq-from

a:ℕ ⟶ ℕ. ∀n:ℕ.  (init0(a)  init0(baire_eq_from(a;n)))


Proof




Definitions occuring in Statement :  baire_eq_from: baire_eq_from(a;k) init0: init0(a) nat: all: x:A. B[x] implies:  Q function: x:A ⟶ B[x]
Definitions unfolded in proof :  so_apply: x[s] so_lambda: λ2x.t[x] top: Top satisfiable_int_formula: satisfiable_int_formula(fmla) decidable: Dec(P) ge: i ≥  assert: b bnot: ¬bb guard: {T} sq_type: SQType(T) or: P ∨ Q exists: x:A. B[x] bfalse: ff subtype_rel: A ⊆B prop: not: ¬A false: False less_than': less_than'(a;b) le: A ≤ B ifthenelse: if then else fi  uimplies: supposing a and: P ∧ Q uiff: uiff(P;Q) btrue: tt it: unit: Unit bool: 𝔹 nat: uall: [x:A]. B[x] member: t ∈ T init0: init0(a) baire_eq_from: baire_eq_from(a;k) implies:  Q all: x:A. B[x]
Lemmas referenced :  int_subtype_base set_subtype_base decidable__le int_formula_prop_wf int_formula_prop_le_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__equal_int nat_properties init0_wf less_than_wf assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal eqff_to_assert le_wf nat_wf equal_wf and_wf false_wf assert_of_lt_int eqtt_to_assert bool_wf lt_int_wf
Rules used in proof :  computeAll voidEquality isect_memberEquality intEquality int_eqEquality functionEquality functionExtensionality voidElimination independent_functionElimination cumulativity instantiate dependent_functionElimination promote_hyp dependent_pairFormation because_Cache lambdaEquality applyEquality applyLambdaEquality dependent_set_memberEquality levelHypothesis addLevel hyp_replacement independent_pairFormation independent_isectElimination productElimination equalitySymmetry equalityTransitivity equalityElimination unionElimination hypothesis hypothesisEquality rename setElimination natural_numberEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut sqequalRule lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n:\mBbbN{}.    (init0(a)  {}\mRightarrow{}  init0(baire\_eq\_from(a;n)))



Date html generated: 2017_04_21-AM-11_24_40
Last ObjectModification: 2017_04_20-PM-06_48_53

Theory : continuity


Home Index