### Nuprl Lemma : gamma-neighbourhood_wf

`∀[beta:ℕ ⟶ ℕ]. ∀[n0:finite-nat-seq()].  (gamma-neighbourhood(beta;n0) ∈ finite-nat-seq() ⟶ (ℕ?))`

Proof

Definitions occuring in Statement :  gamma-neighbourhood: `gamma-neighbourhood(beta;n0)` finite-nat-seq: `finite-nat-seq()` nat: `ℕ` uall: `∀[x:A]. B[x]` unit: `Unit` member: `t ∈ T` function: `x:A ⟶ B[x]` union: `left + right`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` gamma-neighbourhood: `gamma-neighbourhood(beta;n0)` all: `∀x:A. B[x]` implies: `P `` Q` exposed-bfalse: `exposed-bfalse` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` prop: `ℙ` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` nat: `ℕ` le: `A ≤ B` less_than': `less_than'(a;b)` not: `¬A` so_apply: `x[s]` decidable: `Dec(P)`
Lemmas referenced :  init-seg-nat-seq_wf bool_wf eqtt_to_assert it_wf nat_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot finite-nat-seq_wf extend-seq1-all-dec all_wf decidable_wf exists_wf assert_wf append-finite-nat-seq_wf mk-finite-nat-seq_wf false_wf le_wf int_seg_wf not_wf equal-wf-T-base int_seg_subtype_nat unit_wf2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule inrEquality dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination because_Cache voidElimination axiomEquality isect_memberEquality functionEquality applyEquality productEquality dependent_set_memberEquality natural_numberEquality independent_pairFormation intEquality functionExtensionality baseClosed setElimination rename inlEquality

Latex:
\mforall{}[beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[n0:finite-nat-seq()].    (gamma-neighbourhood(beta;n0)  \mmember{}  finite-nat-seq()  {}\mrightarrow{}  (\mBbbN{}?))

Date html generated: 2017_04_20-AM-07_30_26
Last ObjectModification: 2017_02_27-PM-06_00_57

Theory : continuity

Home Index