### Nuprl Lemma : gamma-neighbourhood-prop4

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

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()` int_seg: `{i..j-}` nat: `ℕ` assert: `↑b` isl: `isl(x)` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` unit: `Unit` apply: `f a` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` inl: `inl x` union: `left + right` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` prop: `ℙ` false: `False` subtype_rel: `A ⊆r B` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(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 b then t else f fi ` assert: `↑b` bfalse: `ff` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` cand: `A c∧ B` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` finite-nat-seq: `finite-nat-seq()` pi1: `fst(t)` append-finite-nat-seq: `f**g` init-seg-nat-seq: `init-seg-nat-seq(f;g)` pi2: `snd(t)` ge: `i ≥ j ` int_seg: `{i..j-}` less_than: `a < b` true: `True` squash: `↓T` lelt: `i ≤ j < k` mk-finite-nat-seq: `f^(n)` ext-finite-nat-seq: `ext-finite-nat-seq(f;x)`
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_wf subtype_rel_function nat_wf int_seg_subtype_nat istype-false subtype_rel_self 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 true_wf unit_wf2 assert-init-seg-nat-seq2 nat_properties intformand_wf itermAdd_wf itermVar_wf int_formula_prop_and_lemma int_term_value_add_lemma int_term_value_var_lemma lt_int_wf assert_of_lt_int int_seg_properties istype-less_than iff_weakening_uiff assert_wf less_than_wf istype-top subtract_wf itermSubtract_wf intformless_wf int_term_value_subtract_lemma int_formula_prop_less_lemma decidable__lt int_seg_subtype
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality 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,  because_Cache setElimination rename independent_pairFormation Error :inhabitedIsType,  Error :equalityIstype,  equalityTransitivity equalitySymmetry Error :functionIsType,  equalityElimination productElimination promote_hyp instantiate cumulativity Error :inlEquality_alt,  Error :productIsType,  closedConclusion addEquality int_eqEquality lessCases Error :isect_memberFormation_alt,  axiomSqEquality Error :isectIsTypeImplies,  imageMemberEquality baseClosed imageElimination Error :functionExtensionality_alt

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

Date html generated: 2019_06_20-PM-03_04_28
Last ObjectModification: 2018_12_06-PM-11_34_52

Theory : continuity

Home Index