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

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 :  all: x:A. B[x] member: t ∈ T nat: decidable: Dec(P) or: P ∨ Q uall: [x:A]. B[x] uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T} nat_plus: + ge: i ≥  not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top and: P ∧ Q prop: squash: T so_lambda: λ2x.t[x] so_apply: x[s] subtype_rel: A ⊆B sq_stable: SqStable(P) real-unit-ball: B(n) le: A ≤ B less_than': less_than'(a;b) rev_implies:  Q iff: ⇐⇒ Q ext-eq: A ≡ B
Lemmas referenced :  decidable__equal_int subtype_base_sq int_subtype_base approx-fixpoint-unit-ball-0-ext nat_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformle_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_le_lemma int_formula_prop_wf istype-less_than sq_stable__ex_nat_plus unit-ball-approx_wf nat_plus_properties decidable__le istype-le assert_wf approx-ball-to-ball_wf nat_plus_wf decidable__exists-unit-ball-approx nat_plus_subtype_nat decidable__assert squash_wf rless_wf real-vec-dist_wf real_wf int-to-real_wf real-unit-ball_wf real-vec-sep_wf istype-nat real-unit-ball-0 sq_stable__rless subtype_rel_self subtype_rel_set real-vec_wf rleq_wf real-vec-norm_wf nat_wf set_subtype_base le_wf rless_functionality real-vec-dist-dim0 req_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality hypothesis natural_numberEquality unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination because_Cache independent_functionElimination dependent_set_memberEquality_alt approximateComputation dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation universeIsType productElimination imageElimination productEquality applyEquality imageMemberEquality baseClosed inhabitedIsType equalityTransitivity equalitySymmetry setIsType functionIsType productIsType

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_13
Last ObjectModification: 2019_07_30-PM-00_32_07

Theory : real!vectors


Home Index