---

Step * of Lemma punctured-ball-boundary-retraction

No Annotations
∀n:ℕ. ∀p:{p:ℝ^n| ||p|| < r1} .  Retract({x:ℝ^n| x ≠ p}  ⟶ {x:ℝ^n| ||x|| = r1} )
BY
{ (Auto THEN DVar `p' THEN (Assert ||p|| < r1 BY (Unhide THEN Auto)) THEN Thin (-2) THEN CaseNat 0 `n') }

1
1. n : ℕ
2. p : ℝ^n
3. ||p|| < r1
4. n = 0 ∈ ℤ
⊢ Retract({x:ℝ^0| x ≠ p}  ⟶ {x:ℝ^0| ||x|| = r1} )

2
1. n : ℕ
2. p : ℝ^n
3. ||p|| < r1
4. ¬(n = 0 ∈ ℤ)
⊢ Retract({x:ℝ^n| x ≠ p}  ⟶ {x:ℝ^n| ||x|| = r1} )

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}p:\{p:\mBbbR{}\^{}n|  ||p||  <  r1\}  .    Retract(\{x:\mBbbR{}\^{}n|  x  \mneq{}  p\}    {}\mrightarrow{}  \{x:\mBbbR{}\^{}n|  ||x||  =  r1\}  )


By

---

Latex:
(Auto
  THEN  DVar  `p'
  THEN  (Assert  ||p||  <  r1  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-2)
  THEN  CaseNat  0  `n')

---

Home Index