### Nuprl Lemma : gamma-neighbourhood-prop6

beta:ℕ ⟶ ℕ. ∀n0:finite-nat-seq(). ∀x,n:ℕ.
((¬((beta x) 0 ∈ ℤ))
(↑isl(gamma-neighbourhood(beta;n0) ext-finite-nat-seq(n0**λk.(x 1)^(1);0)^(n)))
((gamma-neighbourhood(beta;n0) ext-finite-nat-seq(n0**λk.(x 1)^(1);0)^(n)) (inl 0) ∈ (ℕ?)))

Proof

Definitions occuring in Statement :  ext-finite-nat-seq: ext-finite-nat-seq(f;x) gamma-neighbourhood: gamma-neighbourhood(beta;n0) append-finite-nat-seq: f**g mk-finite-nat-seq: f^(n) finite-nat-seq: finite-nat-seq() nat: assert: b isl: isl(x) all: x:A. B[x] not: ¬A implies:  Q unit: Unit apply: a lambda: λx.A[x] function: x:A ⟶ B[x] inl: inl x union: left right add: m natural_number: \$n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q uall: [x:A]. B[x] member: t ∈ T nat: decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: false: False int_seg: {i..j-} ge: i ≥  lelt: i ≤ j < k and: P ∧ Q subtype_rel: A ⊆B isl: isl(x) gamma-neighbourhood: gamma-neighbourhood(beta;n0) exposed-bfalse: exposed-bfalse bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  assert: b bfalse: ff sq_type: SQType(T) guard: {T} bnot: ¬bb so_lambda: λ2x.t[x] so_apply: x[s] le: A ≤ B less_than': less_than'(a;b) iff: ⇐⇒ Q finite-nat-seq: finite-nat-seq() mk-finite-nat-seq: f^(n) append-finite-nat-seq: f**g ext-finite-nat-seq: ext-finite-nat-seq(f;x) pi1: fst(t) pi2: snd(t) less_than: a < b true: True squash: T rev_implies:  Q
Lemmas referenced :  istype-assert gamma-neighbourhood_wf mk-finite-nat-seq_wf ext-finite-nat-seq_wf append-finite-nat-seq_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 int_seg_properties nat_properties intformand_wf itermAdd_wf itermVar_wf int_formula_prop_and_lemma int_term_value_add_lemma int_term_value_var_lemma int_seg_wf btrue_wf bfalse_wf istype-nat finite-nat-seq_wf init-seg-nat-seq_wf eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot extend-seq1-all-dec subtype_rel_self nat_wf decidable_wf assert_wf not_wf equal-wf-base set_subtype_base le_wf int_subtype_base int_seg_subtype_nat istype-false subtype_rel_function all_wf exists_wf true_wf decidable__lt intformless_wf intformeq_wf int_formula_prop_less_lemma int_formula_prop_eq_lemma istype-less_than assert-init-seg-nat-seq2 istype-top less_than_anti-reflexive less_than_wf lt_int_wf assert_of_lt_int decidable__equal_int iff_weakening_uiff unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality because_Cache Error :dependent_set_memberEquality_alt,  natural_numberEquality dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  Error :isect_memberEquality_alt,  voidElimination sqequalRule Error :universeIsType,  addEquality setElimination rename productElimination int_eqEquality independent_pairFormation Error :inhabitedIsType,  Error :equalityIstype,  equalityTransitivity equalitySymmetry Error :functionIsType,  equalityElimination promote_hyp instantiate cumulativity functionEquality productEquality intEquality baseClosed closedConclusion Error :productIsType,  hyp_replacement applyLambdaEquality lessCases Error :isect_memberFormation_alt,  axiomSqEquality Error :isectIsTypeImplies,  imageMemberEquality imageElimination baseApply sqequalBase Error :inlEquality_alt

Latex:
\mforall{}beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n0:finite-nat-seq().  \mforall{}x,n:\mBbbN{}.
((\mneg{}((beta  x)  =  0))
{}\mRightarrow{}  (\muparrow{}isl(gamma-neighbourhood(beta;n0)  ext-finite-nat-seq(n0**\mlambda{}k.(x  +  1)\^{}(1);0)\^{}(n)))
{}\mRightarrow{}  ((gamma-neighbourhood(beta;n0)  ext-finite-nat-seq(n0**\mlambda{}k.(x  +  1)\^{}(1);0)\^{}(n))  =  (inl  0)))

Date html generated: 2019_06_20-PM-03_04_43
Last ObjectModification: 2018_12_06-PM-11_34_43

Theory : continuity

Home Index