### Nuprl Lemma : gamma-neighbourhood-prop1

`∀beta:ℕ ⟶ ℕ. ∀n0:finite-nat-seq().`
`  ((∀a:ℕ ⟶ ℕ. ∃x:ℕ. (↑isl(gamma-neighbourhood(beta;n0) a^(x))))`
`  ∧ (∀a,b:finite-nat-seq().`
`       ((↑isl(gamma-neighbourhood(beta;n0) a))`
`       `` ((gamma-neighbourhood(beta;n0) a) = (gamma-neighbourhood(beta;n0) a**b) ∈ (ℕ?)))))`

Proof

Definitions occuring in Statement :  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]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` unit: `Unit` apply: `f a` function: `x:A ⟶ B[x]` union: `left + right` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` member: `t ∈ T` implies: `P `` Q` uall: `∀[x:A]. B[x]` isl: `isl(x)` exists: `∃x:A. B[x]` nat: `ℕ` finite-nat-seq: `finite-nat-seq()` pi1: `fst(t)` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` guard: `{T}` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` uiff: `uiff(P;Q)` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` prop: `ℙ` subtype_rel: `A ⊆r B` gamma-neighbourhood: `gamma-neighbourhood(beta;n0)` ifthenelse: `if b then t else f fi ` btrue: `tt` assert: `↑b` bfalse: `ff` init-seg-nat-seq: `init-seg-nat-seq(f;g)` iff: `P `⇐⇒` Q` mk-finite-nat-seq: `f^(n)` append-finite-nat-seq: `f**g` pi2: `snd(t)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` true: `True` exposed-bfalse: `exposed-bfalse` bool: `𝔹` unit: `Unit` it: `⋅` sq_type: `SQType(T)` bnot: `¬bb` squash: `↓T` rev_implies: `P `` Q`
Lemmas referenced :  istype-assert gamma-neighbourhood_wf btrue_wf bfalse_wf finite-nat-seq_wf istype-nat add_nat_wf istype-false istype-le nat_properties decidable__le add-is-int-iff full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_wf false_wf mk-finite-nat-seq_wf subtype_rel_function nat_wf int_seg_wf int_seg_subtype_nat subtype_rel_self bool_cases_sqequal init-seg-nat-seq_wf assert_of_tt assert-init-seg-nat-seq extend-seq1-all-dec all_wf decidable_wf exists_wf assert_wf append-finite-nat-seq_wf not_wf equal-wf-base set_subtype_base le_wf int_subtype_base eqtt_to_assert eqff_to_assert subtype_base_sq bool_wf bool_subtype_base assert-bnot init-seg-nat-seq-append-implies-left decidable__equal_int unit_wf2 true_wf init-seg-nat-seq-append-implies-right decidable__exists_int_seg decidable__not equal_wf squash_wf istype-universe iff_weakening_equal append-finite-nat-seq-1
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut Error :inhabitedIsType,  hypothesisEquality independent_pairFormation hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin applyEquality unionElimination sqequalRule Error :equalityIstype,  equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination Error :universeIsType,  Error :functionIsType,  Error :dependent_pairFormation_alt,  Error :dependent_set_memberEquality_alt,  addEquality productElimination setElimination rename closedConclusion natural_numberEquality applyLambdaEquality pointwiseFunctionality promote_hyp baseApply baseClosed independent_isectElimination approximateComputation Error :lambdaEquality_alt,  int_eqEquality Error :isect_memberEquality_alt,  voidElimination because_Cache instantiate functionEquality productEquality intEquality equalityElimination cumulativity Error :inlEquality_alt,  Error :productIsType,  sqequalBase Error :equalityIsType1,  Error :inrFormation_alt,  Error :inlFormation_alt,  Error :unionIsType,  imageElimination universeEquality imageMemberEquality

Latex:
\mforall{}beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n0:finite-nat-seq().
((\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}x:\mBbbN{}.  (\muparrow{}isl(gamma-neighbourhood(beta;n0)  a\^{}(x))))
\mwedge{}  (\mforall{}a,b:finite-nat-seq().
((\muparrow{}isl(gamma-neighbourhood(beta;n0)  a))
{}\mRightarrow{}  ((gamma-neighbourhood(beta;n0)  a)  =  (gamma-neighbourhood(beta;n0)  a**b)))))

Date html generated: 2019_06_20-PM-03_03_53
Last ObjectModification: 2018_11_28-AM-08_57_16

Theory : continuity

Home Index