Nuprl Lemma : unit-ball-approx0

[k:ℕ]. unit-ball-approx(0;k) ≡ Top


Proof




Definitions occuring in Statement :  unit-ball-approx: unit-ball-approx(n;k) nat: ext-eq: A ≡ B uall: [x:A]. B[x] top: Top natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B top: Top nat: le: A ≤ B less_than': less_than'(a;b) not: ¬A implies:  Q false: False unit-ball-approx: unit-ball-approx(n;k) sum: Σ(f[x] x < k) sum_aux: sum_aux(k;v;i;x.f[x]) int_seg: {i..j-} lelt: i ≤ j < k ge: i ≥  uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] all: x:A. B[x] prop:
Lemmas referenced :  istype-void unit-ball-approx_wf istype-le int_seg_properties nat_properties full-omega-unsat intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf istype-int int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf int_seg_wf mul_bounds_1a istype-top istype-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut independent_pairFormation lambdaEquality_alt isect_memberEquality_alt voidElimination extract_by_obid hypothesis universeIsType sqequalHypSubstitution isectElimination thin dependent_set_memberEquality_alt natural_numberEquality sqequalRule lambdaFormation_alt hypothesisEquality functionExtensionality setElimination rename productElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality dependent_functionElimination multiplyEquality because_Cache independent_pairEquality axiomEquality applyEquality

Latex:
\mforall{}[k:\mBbbN{}].  unit-ball-approx(0;k)  \mequiv{}  Top



Date html generated: 2019_10_30-AM-11_28_04
Last ObjectModification: 2019_07_30-AM-11_25_27

Theory : real!vectors


Home Index