Nuprl Lemma : remove-singularity-mfun

∀[X:Type]. ∀[d:metric(X)].
  ∀k:ℕ. ∀f:{p:ℝ^k| r0 < ||p||}  ⟶ X. ∀z:X.
    ((∃c:{c:ℝ| r0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m)))))
    ⇒ mcomplete(X with d)
    ⇒ (∃g:ℝ^k ⟶ X
         ((∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z))
         ∧ (∀p:{p:ℝ^k| r0 < ||p||} . g p ≡ f p)
         ∧ (f:FUN({p:ℝ^k| r0 < ||p||} ;X) ⇒ g:FUN(ℝ^k;X)))))


Proof



Definitions occuring in Statement :  rn-metric: rn-metric(n),  real-vec-norm: ||x||,  req-vec: req-vec(n;x;y),  real-vec: ℝ^n,  mcomplete: mcomplete(M),  is-mfun: f:FUN(X;Y),  mk-metric-space: X with d,  mdist: mdist(d;x;y),  meq: x ≡ y,  metric: metric(X),  rdiv: (x/y),  rleq: x ≤ y,  rless: x < y,  int-to-real: r(n),  real: ℝ,  nat_plus: ℕ+,  nat: ℕ,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  set: {x:A| B[x]} ,  apply: f a,  lambda: λx.A[x],  function: x:A ⟶ B[x],  natural_number: $n,  universe: Type
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  all: ∀x:A. B[x],  implies: P ⇒ Q,  exists: ∃x:A. B[x],  and: P ∧ Q,  cand: A c∧ B,  is-mfun: f:FUN(X;Y),  so_apply: x[s],  prop: ℙ,  meq: x ≡ y,  metric: metric(X),  subtype_rel: A ⊆r B,  uimplies: b supposing a,  real-vec: ℝ^n,  int_seg: {i..j-},  lelt: i ≤ j < k,  le: A ≤ B,  nat: ℕ,  nat_plus: ℕ+,  rneq: x ≠ y,  guard: {T},  or: P ∨ Q,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  ge: i ≥ j ,  decidable: Dec(P),  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  false: False,  top: Top,  stable: Stable{P},  rn-metric: rn-metric(n),  uiff: uiff(P;Q),  rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  remove-singularity,  meq_wf,  real-vec_wf,  rn-metric_wf,  req_witness,  int-to-real_wf,  is-mfun_wf,  rless_wf,  real-vec-norm_wf,  metric-on-subtype,  req-vec_wf,  int_seg_wf,  mcomplete_wf,  mk-metric-space_wf,  real_wf,  rleq_wf,  nat_plus_wf,  rdiv_wf,  rless-int,  nat_plus_properties,  nat_properties,  decidable__lt,  full-omega-unsat,  intformand_wf,  intformnot_wf,  intformless_wf,  itermConstant_wf,  itermVar_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_wf,  mdist_wf,  istype-nat,  metric_wf,  istype-universe,  stable__meq,  false_wf,  not_wf,  not-rless,  minimal-double-negation-hyp-elim,  minimal-not-not-excluded-middle,  real-vec-dist-identity,  meq_functionality,  rless_functionality,  req_weakening,  real-vec-norm_functionality,  req-vec_inversion,  rleq_antisymmetry,  real-vec-norm-nonneg,  real-vec-norm-is-0,  req-vec_functionality,  req-vec_weakening,  meq-same
Rules used in proof :  cut,  introduction,  extract_by_obid,  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  hypothesis,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  lambdaFormation_alt,  dependent_functionElimination,  independent_functionElimination,  productElimination,  dependent_pairFormation_alt,  independent_pairFormation,  sqequalRule,  universeIsType,  inhabitedIsType,  lambdaEquality_alt,  applyEquality,  setElimination,  rename,  natural_numberEquality,  functionIsTypeImplies,  setEquality,  independent_isectElimination,  setIsType,  because_Cache,  productIsType,  functionIsType,  closedConclusion,  inrFormation_alt,  unionElimination,  approximateComputation,  int_eqEquality,  isect_memberEquality_alt,  voidElimination,  instantiate,  universeEquality,  unionEquality,  functionEquality,  unionIsType,  dependent_set_memberEquality_alt
Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].
    \mforall{}k:\mBbbN{}.  \mforall{}f:\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}    {}\mrightarrow{}  X.  \mforall{}z:X.
        ((\mexists{}c:\{c:\mBbbR{}|  r0  \mleq{}  c\} 
              \mforall{}m:\mBbbN{}\msupplus{}.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  .    ((||p||  \mleq{}  (r(4)/r(m)))  {}\mRightarrow{}  (mdist(d;f  p;z)  \mleq{}  (c/r(m)))))
        {}\mRightarrow{}  mcomplete(X  with  d)
        {}\mRightarrow{}  (\mexists{}g:\mBbbR{}\^{}k  {}\mrightarrow{}  X
                  ((\mforall{}p:\mBbbR{}\^{}k.  (req-vec(k;p;\mlambda{}i.r0)  {}\mRightarrow{}  g  p  \mequiv{}  z))
                  \mwedge{}  (\mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  .  g  p  \mequiv{}  f  p)
                  \mwedge{}  (f:FUN(\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  ;X)  {}\mRightarrow{}  g:FUN(\mBbbR{}\^{}k;X)))))


Date html generated: 2019_10_30-AM-11_24_48
Last ObjectModification: 2019_07_02-PM-00_25_15

Theory : real!vectors


Home Index