### Nuprl Lemma : nat-inf-limit

`∀p:ℕ∞ ⟶ 𝔹. ((∀n:ℕ. p n∞ = ff) `` p ∞ = ff)`

Proof

Definitions occuring in Statement :  nat-inf-infinity: `∞` nat2inf: `n∞` nat-inf: `ℕ∞` nat: `ℕ` bfalse: `ff` bool: `𝔹` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uall: `∀[x:A]. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` not: `¬A` false: `False` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` nat-inf: `ℕ∞` nat: `ℕ` ge: `i ≥ j ` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` prop: `ℙ` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` squash: `↓T` so_apply: `x[s]` rev_uimplies: `rev_uimplies(P;Q)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` subtype_rel: `A ⊆r B` less_than': `less_than'(a;b)` true: `True` subtract: `n - m` nat2inf: `n∞` nat-inf-infinity: `∞`
Lemmas referenced :  nat-inf-infinity_wf eqtt_to_assert no-weak-limited-omniscience eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot bfalse_wf istype-nat nat2inf_wf nat-inf_wf bnot_wf b-exists_wf nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf istype-le int_seg_properties int_seg_wf assert_of_bnot assert-b-exists istype-assert decidable__lt intformless_wf int_formula_prop_less_lemma istype-less_than decidable__equal_int subtract_wf set_subtype_base lelt_wf int_subtype_base intformeq_wf itermSubtract_wf int_formula_prop_eq_lemma int_term_value_subtract_lemma subtype_rel_self int_seg_subtype_nat istype-false btrue_wf equal-wf-T-base nat_wf le_wf primrec-wf2 decidable__exists_int_seg decidable__equal_bool easy-member-int_seg add-associates add-swap add-commutes zero-add iff_imp_equal_bool lt_int_wf istype-void iff_weakening_uiff assert_wf not_wf less_than_wf assert_of_lt_int istype-true assert_elim btrue_neq_bfalse assert_functionality_wrt_uiff
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut applyEquality hypothesisEquality introduction extract_by_obid hypothesis inhabitedIsType thin sqequalHypSubstitution unionElimination equalityElimination isectElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination independent_functionElimination voidElimination dependent_pairFormation_alt equalityIstype promote_hyp dependent_functionElimination instantiate cumulativity because_Cache sqequalRule functionIsType universeIsType dependent_set_memberEquality_alt lambdaEquality_alt addEquality setElimination rename natural_numberEquality approximateComputation int_eqEquality Error :memTop,  independent_pairFormation imageElimination productIsType intEquality applyLambdaEquality hypothesis_subsumption functionEquality productEquality baseClosed baseApply closedConclusion setIsType imageMemberEquality sqequalBase inlFormation_alt inrFormation_alt hyp_replacement

Latex:
\mforall{}p:\mBbbN{}\minfty{}  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}n:\mBbbN{}.  p  n\minfty{}  =  ff)  {}\mRightarrow{}  p  \minfty{}  =  ff)

Date html generated: 2020_05_20-AM-07_47_51
Last ObjectModification: 2020_02_28-PM-02_49_04

Theory : basic

Home Index