Nuprl Lemma : approx-fixpoint-unit-ball-0

n:ℕ+. ∀f:{f:B(n) ⟶ B(n)| 
           (∀e:{e:ℝr0 < e} . ∃del:{del:ℝr0 < del} . ∀x,y:B(n).  ((d(x;y) < del)  (d(f x;f y) < e)))
           ∧ (∀x:B(n). x ≠ x))} . ∀e:{e:ℝr0 < e} .
  ∃t:B(n) ⟶ 𝔹
   ((∀p:B(n). ((↑(t p))  (↓d(f p;p) < e))) ∧ (↓∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑(t approx-ball-to-ball(k;q)))))


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) real-vec-sep: a ≠ b real-vec-dist: d(x;y) rless: x < y int-to-real: r(n) real: nat_plus: + assert: b bool: 𝔹 all: x:A. B[x] exists: x:A. B[x] not: ¬A squash: T implies:  Q and: P ∧ Q set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] natural_number: $n
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] uimplies: supposing a rneq: x ≠ y guard: {T} or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True nat: nat_plus: + rless: x < y sq_exists: x:A [B[x]] decidable: Dec(P) not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top prop: subtype_rel: A ⊆B real-unit-ball: B(n) isr: isr(x) assert: b ifthenelse: if then else fi  bfalse: ff btrue: tt sq_stable: SqStable(P) sq_type: SQType(T) int_nzero: -o nequal: a ≠ b ∈  rdiv: (x/y) uiff: uiff(P;Q) req_int_terms: t1 ≡ t2 cand: c∧ B so_lambda: λ2x.t[x] so_apply: x[s] real-vec-sep: a ≠ b rge: x ≥ y stable: Stable{P}
Lemmas referenced :  rmul_preserves_rless rdiv_wf rless-int rless-cases rmul_wf int-to-real_wf real-vec-dist_wf nat_plus_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 real-unit-ball_wf istype-true bfalse_wf btrue_wf nat_plus_subtype_nat istype-assert squash_wf rless_wf nat_plus_wf unit-ball-approx_wf assert_wf approx-ball-to-ball_wf real_wf real-vec-sep_wf itermSubtract_wf itermMultiply_wf rinv_wf2 sq_stable__rless subtype_base_sq int_subtype_base decidable__equal_int intformeq_wf int_formula_prop_eq_lemma int_term_value_mul_lemma nequal_wf radd-preserves-rless radd_wf itermAdd_wf rless_functionality 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 int-rinv-cancel real_term_value_add_lemma small-reciprocal-real rmin_wf rmin_strict_ub rmin-rleq rless_transitivity1 decidable__lt real-unit-ball-totally-bounded1 mul_nat_plus istype-less_than decidable__exists-unit-ball-approx multiply_nat_wf decidable__assert isr_wf rneq-int rless_transitivity2 rsub_wf rless-implies-rless rleq_weakening rleq_wf rless_functionality_wrt_implies rleq_weakening_equal stable__rleq false_wf not_wf not-rless minimal-double-negation-hyp-elim minimal-not-not-excluded-middle real-vec-triangle-inequality real-vec-dist-symmetry req_weakening rleq_weakening_rless radd_functionality_wrt_rless2 radd_functionality_wrt_rleq radd_functionality_wrt_rless1 rless_irreflexivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin because_Cache isectElimination independent_isectElimination sqequalRule hypothesis inrFormation_alt productElimination independent_functionElimination natural_numberEquality independent_pairFormation imageMemberEquality hypothesisEquality baseClosed closedConclusion dependent_set_memberEquality_alt setElimination rename unionElimination approximateComputation dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination universeIsType applyEquality inhabitedIsType equalityTransitivity equalitySymmetry functionExtensionality equalityIstype functionIsType productIsType productEquality setIsType imageElimination instantiate cumulativity intEquality sqequalBase minusEquality multiplyEquality unionEquality functionEquality unionIsType

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}f:\{f:B(n)  {}\mrightarrow{}  B(n)| 
                      (\mforall{}e:\{e:\mBbbR{}|  r0  <  e\} 
                            \mexists{}del:\{del:\mBbbR{}|  r0  <  del\}  .  \mforall{}x,y:B(n).    ((d(x;y)  <  del)  {}\mRightarrow{}  (d(f  x;f  y)  <  e)))
                      \mwedge{}  (\mneg{}(\mforall{}x:B(n).  f  x  \mneq{}  x))\}  .  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
    \mexists{}t:B(n)  {}\mrightarrow{}  \mBbbB{}
      ((\mforall{}p:B(n).  ((\muparrow{}(t  p))  {}\mRightarrow{}  (\mdownarrow{}d(f  p;p)  <  e)))
      \mwedge{}  (\mdownarrow{}\mexists{}k:\mBbbN{}\msupplus{}.  \mexists{}q:unit-ball-approx(n;k).  (\muparrow{}(t  approx-ball-to-ball(k;q)))))



Date html generated: 2019_10_30-AM-11_29_07
Last ObjectModification: 2019_07_30-PM-00_30_01

Theory : real!vectors


Home Index