Nuprl Lemma : approx-fixpoint-unit-ball-1-ext

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} .
  ∃p:B(n). (↓d(f p;p) < e)


Proof




Definitions occuring in Statement :  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: 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 :  member: t ∈ T it: approx-ball-to-ball: approx-ball-to-ball(k;p) int-rdiv: (a)/k1 outl: outl(x) bottom: let: let approx-fixpoint-unit-ball-1 decidable__equal_int approx-fixpoint-unit-ball-0-ext sq_stable__ex_nat_plus decidable__exists-unit-ball-approx decidable__assert decidable__int_equal sq_stable__ex_int_upper uall: [x:A]. B[x] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2x.t[x] top: Top so_apply: x[s] uimplies: supposing a so_lambda: λ2y.t[x; y] so_apply: x[s1;s2]
Lemmas referenced :  approx-fixpoint-unit-ball-1 lifting-strict-int_eq istype-void strict4-decide lifting-strict-decide strict4-spread decidable__equal_int approx-fixpoint-unit-ball-0-ext sq_stable__ex_nat_plus decidable__exists-unit-ball-approx decidable__assert decidable__int_equal sq_stable__ex_int_upper
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed isect_memberEquality_alt voidElimination independent_isectElimination

Latex:
\mforall{}n:\mBbbN{}.  \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{}p:B(n).  (\mdownarrow{}d(f  p;p)  <  e)



Date html generated: 2019_10_30-AM-11_29_16
Last ObjectModification: 2019_07_30-PM-00_49_17

Theory : real!vectors


Home Index