Nuprl Lemma : extend-approx-ball_wf

[k,n:ℕ]. ∀[p:unit-ball-approx(n;k)]. ∀[z:{-k..k 1-}].
  extend-approx-ball(n;p;z) ∈ unit-ball-approx(n 1;k) supposing ((p i) (p i) i < n) (z z)) ≤ (k k)


Proof




Definitions occuring in Statement :  extend-approx-ball: extend-approx-ball(n;p;z) unit-ball-approx: unit-ball-approx(n;k) sum: Σ(f[x] x < k) int_seg: {i..j-} nat: uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B member: t ∈ T apply: a multiply: m add: m minus: -n natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a unit-ball-approx: unit-ball-approx(n;k) extend-approx-ball: extend-approx-ball(n;p;z) int_seg: {i..j-} all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q lelt: i ≤ j < k le: A ≤ B less_than: a < b squash: T nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top prop: bfalse: ff so_lambda: λ2x.t[x] subtype_rel: A ⊆B so_apply: x[s] less_than': less_than'(a;b) true: True sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b rev_implies:  Q iff: ⇐⇒ Q
Lemmas referenced :  lt_int_wf eqtt_to_assert assert_of_lt_int int_seg_properties nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_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_formula_prop_wf istype-le istype-less_than int_seg_wf sum_wf itermAdd_wf int_term_value_add_lemma unit-ball-approx_wf istype-nat sum-unroll decidable__lt intformless_wf int_formula_prop_less_lemma istype-top subtract_wf subtype_base_sq int_subtype_base add-subtract-cancel eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf less_than_wf squash_wf true_wf decidable__equal_int intformeq_wf int_formula_prop_eq_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut dependent_set_memberEquality_alt lambdaEquality_alt sqequalHypSubstitution setElimination thin rename because_Cache hypothesis extract_by_obid isectElimination inhabitedIsType lambdaFormation_alt unionElimination equalityElimination sqequalRule productElimination independent_isectElimination applyEquality independent_pairFormation imageElimination hypothesisEquality dependent_functionElimination natural_numberEquality approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination universeIsType productIsType equalityIstype equalityTransitivity equalitySymmetry addEquality multiplyEquality axiomEquality isectIsTypeImplies minusEquality lessCases axiomSqEquality imageMemberEquality baseClosed instantiate cumulativity intEquality promote_hyp functionIsType

Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[p:unit-ball-approx(n;k)].  \mforall{}[z:\{-k..k  +  1\msupminus{}\}].
    extend-approx-ball(n;p;z)  \mmember{}  unit-ball-approx(n  +  1;k) 
    supposing  (\mSigma{}((p  i)  *  (p  i)  |  i  <  n)  +  (z  *  z))  \mleq{}  (k  *  k)



Date html generated: 2019_10_30-AM-11_28_14
Last ObjectModification: 2019_06_28-PM-01_56_14

Theory : real!vectors


Home Index