Nuprl Lemma : Kripke2b

a:ℕ ⟶ ℕ(is-absolutely-free{i:l}(a)  init0(a)  increasing-sequence(a)  (∀m:ℕ. ∃n:ℕ((a n) ≥ ))))


Proof




Definitions occuring in Statement :  is-absolutely-free: is-absolutely-free{i:l}(f) init0: init0(a) increasing-sequence: increasing-sequence(a) nat: ge: i ≥  all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q apply: a function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q not: ¬A false: False exists: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B nat: ge: i ≥  prop: is-absolutely-free: is-absolutely-free{i:l}(f) uimplies: supposing a le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) iff: ⇐⇒ Q rev_implies:  Q decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) zero-seq: 0s int_seg: {i..j-} lelt: i ≤ j < k kripke2b-baire-seq: kripke2b-baire-seq(a;x;F) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b nequal: a ≠ b ∈  true: True init0: init0(a) cantor2baire-aux: cantor2baire-aux(a;n) cantor2baire: cantor2baire(a) change-from1: change-from1(a) pi1: fst(t) label: ...$L... t squash: T min-inc-seq: min-inc-seq(a;n;k) baire_eq_from: baire_eq_from(a;k)
Lemmas referenced :  istype-nat ge_wf increasing-sequence_wf init0_wf is-absolutely-free_wf nat_wf not-quotient-true equal_wf int_seg_wf subtype_rel_function int_seg_subtype_nat istype-false subtype_rel_self add_nat_wf decidable__le full-omega-unsat intformnot_wf intformle_wf itermConstant_wf istype-int int_formula_prop_not_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf istype-le nat_properties intformand_wf itermVar_wf itermAdd_wf intformeq_wf int_formula_prop_and_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma false_wf strong-continuity2-implies-uniform-continuity2-nat kripke2b-baire-seq_wf decidable__lt intformless_wf int_formula_prop_less_lemma decidable__equal_nat subtype_base_sq set_subtype_base le_wf int_subtype_base init0-implies-eq-upto1-zero-seq zero-seq_wf baire2cantor_wf change-from1_wf int_seg_properties eq-finite-seqs_wf cantor2baire_wf eqtt_to_assert eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int assert_of_eq_int eq_int_wf primrec1_lemma subtype_rel_wf istype-less_than decidable__equal_int eq-finite-seqs-iff-eq-upto min-inc-seq_wf iff_weakening_equal squash_wf true_wf istype-universe baire2cantor2baire pi1_wf min-increasing-sequence_wf min-increasing-sequence-prop2 baire-diff-from_wf implies-eq-upto-baire2cantor eq-upto-baire-diff-from increasing-baire-diff-from init0-baire-diff-from baire-diff-from-diff baire_eq_from_wf eq-upto-baire-eq-from less_than_wf assert_wf iff_weakening_uiff assert_of_lt_int lt_int_wf increasing-sequence-prop1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut thin because_Cache hypothesis sqequalHypSubstitution independent_functionElimination voidElimination sqequalRule Error :functionIsType,  introduction extract_by_obid Error :productIsType,  Error :universeIsType,  isectElimination applyEquality hypothesisEquality Error :lambdaEquality_alt,  setElimination rename Error :inhabitedIsType,  dependent_functionElimination functionEquality productEquality natural_numberEquality independent_isectElimination independent_pairFormation productElimination Error :equalityIstype,  Error :dependent_set_memberEquality_alt,  addEquality unionElimination approximateComputation Error :dependent_pairFormation_alt,  Error :isect_memberEquality_alt,  equalityTransitivity equalitySymmetry applyLambdaEquality pointwiseFunctionality promote_hyp int_eqEquality Error :functionExtensionality_alt,  Error :setIsType,  instantiate cumulativity intEquality closedConclusion equalityElimination int_eqReduceFalseSq int_eqReduceTrueSq hyp_replacement baseApply sqequalBase baseClosed functionExtensionality setEquality imageElimination imageMemberEquality universeEquality

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
    (is-absolutely-free\{i:l\}(a)
    {}\mRightarrow{}  init0(a)
    {}\mRightarrow{}  increasing-sequence(a)
    {}\mRightarrow{}  (\mneg{}(\mforall{}m:\mBbbN{}.  \mexists{}n:\mBbbN{}.  ((a  n)  \mgeq{}  m  ))))



Date html generated: 2019_06_20-PM-03_07_58
Last ObjectModification: 2018_12_06-PM-11_57_04

Theory : continuity


Home Index