Nuprl Lemma : punctured-ball-boundary-retraction
∀n:ℕ. ∀p:{p:ℝ^n| ||p|| < r1} . Retract({x:ℝ^n| x ≠ p} ⟶ {x:ℝ^n| ||x|| = r1} )
Proof
Definitions occuring in Statement :
real-vec-sep: a ≠ b,
rn-metric: rn-metric(n),
real-vec-norm: ||x||,
real-vec: ℝ^n,
m-retraction: Retract(X ⟶ A),
rless: x < y,
req: x = y,
int-to-real: r(n),
nat: ℕ,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
sq_stable: SqStable(P),
implies: P ⇒ Q,
squash: ↓T,
nat: ℕ,
decidable: Dec(P),
or: P ∨ Q,
uimplies: b supposing a,
sq_type: SQType(T),
guard: {T},
prop: ℙ,
not: ¬A,
false: False,
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
so_apply: x[s],
ge: i ≥ j ,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
top: Top,
iff: P ⇐⇒ Q,
int_seg: {i..j-},
rless: x < y,
sq_exists: ∃x:A [B[x]],
nat_plus: ℕ+,
lelt: i ≤ j < k,
real: ℝ,
real-vec-norm: ||x||,
dot-product: x⋅y,
subtract: n - m,
less_than: a < b,
true: True,
m-retraction: Retract(X ⟶ A),
cand: A c∧ B,
is-mfun: f:FUN(X;Y),
uiff: uiff(P;Q),
let: let,
real-vec-sep: a ≠ b,
rsqrt: rsqrt(x),
rroot: rroot(i;x),
ifthenelse: if b then t else f fi ,
isEven: isEven(n),
eq_int: (i =z j),
modulus: a mod n,
remainder: n rem m,
btrue: tt,
rroot-abs: rroot-abs(i;x),
fastexp: i^n,
efficient-exp-ext,
genrec: genrec,
real-vec-dist: d(x;y),
rneq: x ≠ y,
rev_implies: P ⇐ Q,
rev_uimplies: rev_uimplies(P;Q),
req_int_terms: t1 ≡ t2,
rge: x ≥ y,
req-vec: req-vec(n;x;y),
real-vec-sub: X - Y,
real-vec-mul: a*X,
real-vec-add: X + Y,
real-vec: ℝ^n
Latex:
\mforall{}n:\mBbbN{}. \mforall{}p:\{p:\mBbbR{}\^{}n| ||p|| < r1\} . Retract(\{x:\mBbbR{}\^{}n| x \mneq{} p\} {}\mrightarrow{} \{x:\mBbbR{}\^{}n| ||x|| = r1\} )
Date html generated:
2020_05_20-PM-00_52_48
Last ObjectModification:
2019_11_11-PM-02_32_17
Theory : reals
Home
Index