Nuprl Lemma : approx-ball-to-ball_wf

[n:ℕ]. ∀[k:ℕ+]. ∀[p:unit-ball-approx(n;k)].  (approx-ball-to-ball(k;p) ∈ B(n))


Proof




Definitions occuring in Statement :  approx-ball-to-ball: approx-ball-to-ball(k;p) unit-ball-approx: unit-ball-approx(n;k) real-unit-ball: B(n) nat_plus: + nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T approx-ball-to-ball: approx-ball-to-ball(k;p) real-vec: ^n subtype_rel: A ⊆B unit-ball-approx: unit-ball-approx(n;k) int_seg: {i..j-} nat: real-unit-ball: B(n) all: x:A. B[x] prop: nat_plus: + ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top and: P ∧ Q iff: ⇐⇒ Q le: A ≤ B less_than': less_than'(a;b) dot-product: x⋅y rev_implies:  Q so_lambda: λ2x.t[x] lelt: i ≤ j < k less_than: a < b squash: T so_apply: x[s] rneq: x ≠ y guard: {T} uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) pointwise-req: x[k] y[k] for k ∈ [n,m] nequal: a ≠ b ∈  rat_term_to_real: rat_term_to_real(f;t) rtermMultiply: left "*" right rat_term_ind: rat_term_ind rtermDivide: num "/" denom rtermVar: rtermVar(var) rtermConstant: "const" pi1: fst(t) true: True pi2: snd(t) sq_stable: SqStable(P) rdiv: (x/y) req_int_terms: t1 ≡ t2
Lemmas referenced :  int-rdiv_wf nat_plus_inc_int_nzero int-to-real_wf int_seg_wf square-rleq-1-iff real-vec-norm_wf rleq_wf unit-ball-approx_wf nat_plus_properties nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformless_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_less_lemma int_formula_prop_wf istype-le nat_plus_wf istype-nat rabs_wf real-vec-norm-nonneg rnexp_wf dot-product_wf iff_weakening_uiff rleq_functionality rabs-of-nonneg req_weakening real-vec-norm-squared rsum_wf subtract_wf rmul_wf int_seg_properties decidable__lt itermAdd_wf itermSubtract_wf int_term_value_add_lemma int_term_value_subtract_lemma istype-less_than rdiv_wf subtract-add-cancel rless-int rless_wf rsum_functionality2 rmul_functionality int-rdiv-req sum_wf rleq-int rmul-int rsum_int rsum_functionality mul_bounds_1b rneq_functionality rneq-int int_entire_a intformeq_wf int_formula_prop_eq_lemma int_subtype_base req_functionality rmul-rdiv mul_nat_plus assert-rat-term-eq2 rtermDivide_wf rtermVar_wf rtermMultiply_wf rtermConstant_wf rdiv_functionality rsum_linearity2 rmul_preserves_rleq sq_stable__rless rinv_wf2 itermMultiply_wf req_transitivity rmul-rinv3 req-iff-rsub-is-0 real_polynomial_null real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_const_lemma real_term_value_var_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule lambdaEquality_alt extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality hypothesis setElimination rename inhabitedIsType equalityTransitivity equalitySymmetry universeIsType natural_numberEquality dependent_set_memberEquality_alt dependent_functionElimination axiomEquality unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation isectIsTypeImplies because_Cache productElimination lambdaFormation_alt promote_hyp imageElimination productIsType addEquality closedConclusion inrFormation_alt multiplyEquality equalityIstype baseClosed sqequalBase applyLambdaEquality imageMemberEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[p:unit-ball-approx(n;k)].    (approx-ball-to-ball(k;p)  \mmember{}  B(n))



Date html generated: 2019_10_30-AM-11_28_44
Last ObjectModification: 2019_06_28-PM-01_56_23

Theory : real!vectors


Home Index