Step
*
1
2
of Lemma
remove-singularity-mfun
1. X : Type
2. d : metric(X)
3. k : ℕ
4. f : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. z : X
6. ∃c:{c:ℝ| r0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) 
⇒ (mdist(d;f p;z) ≤ (c/r(m))))
7. mcomplete(X with d)
8. g : ℝ^k ⟶ X
9. ∀p:ℝ^k. (req-vec(k;p;λi.r0) 
⇒ g p ≡ z)
10. ∀p:{p:ℝ^k| r0 < ||p||} . g p ≡ f p
11. ∀p:ℝ^k. (req-vec(k;p;λi.r0) 
⇒ g p ≡ z)
12. ∀p:{p:ℝ^k| r0 < ||p||} . g p ≡ f p
13. ∀x1,x2:{p:ℝ^k| r0 < ||p||} .  (x1 ≡ x2 
⇒ f x1 ≡ f x2)
14. x1 : ℝ^k
15. x2 : ℝ^k
16. x1 ≡ x2
17. ¬(r0 < ||x1||)
18. ||x1|| ≤ r0
⊢ g x1 ≡ g x2
BY
{ ((Assert ||x1|| = r0 BY (BLemma `rleq_antisymmetry` THEN Auto)) THEN (RWO  "real-vec-norm-is-0" (-1) THENA Auto)) }
1
1. X : Type
2. d : metric(X)
3. k : ℕ
4. f : {p:ℝ^k| r0 < ||p||}  ⟶ X
5. z : X
6. ∃c:{c:ℝ| r0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m))) 
⇒ (mdist(d;f p;z) ≤ (c/r(m))))
7. mcomplete(X with d)
8. g : ℝ^k ⟶ X
9. ∀p:ℝ^k. (req-vec(k;p;λi.r0) 
⇒ g p ≡ z)
10. ∀p:{p:ℝ^k| r0 < ||p||} . g p ≡ f p
11. ∀p:ℝ^k. (req-vec(k;p;λi.r0) 
⇒ g p ≡ z)
12. ∀p:{p:ℝ^k| r0 < ||p||} . g p ≡ f p
13. ∀x1,x2:{p:ℝ^k| r0 < ||p||} .  (x1 ≡ x2 
⇒ f x1 ≡ f x2)
14. x1 : ℝ^k
15. x2 : ℝ^k
16. x1 ≡ x2
17. ¬(r0 < ||x1||)
18. ||x1|| ≤ r0
19. req-vec(k;x1;λi.r0)
⊢ g x1 ≡ g x2
Latex:
Latex:
1.  X  :  Type
2.  d  :  metric(X)
3.  k  :  \mBbbN{}
4.  f  :  \{p:\mBbbR{}\^{}k|  r0  <  ||p||\}    {}\mrightarrow{}  X
5.  z  :  X
6.  \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))))
7.  mcomplete(X  with  d)
8.  g  :  \mBbbR{}\^{}k  {}\mrightarrow{}  X
9.  \mforall{}p:\mBbbR{}\^{}k.  (req-vec(k;p;\mlambda{}i.r0)  {}\mRightarrow{}  g  p  \mequiv{}  z)
10.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  .  g  p  \mequiv{}  f  p
11.  \mforall{}p:\mBbbR{}\^{}k.  (req-vec(k;p;\mlambda{}i.r0)  {}\mRightarrow{}  g  p  \mequiv{}  z)
12.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  .  g  p  \mequiv{}  f  p
13.  \mforall{}x1,x2:\{p:\mBbbR{}\^{}k|  r0  <  ||p||\}  .    (x1  \mequiv{}  x2  {}\mRightarrow{}  f  x1  \mequiv{}  f  x2)
14.  x1  :  \mBbbR{}\^{}k
15.  x2  :  \mBbbR{}\^{}k
16.  x1  \mequiv{}  x2
17.  \mneg{}(r0  <  ||x1||)
18.  ||x1||  \mleq{}  r0
\mvdash{}  g  x1  \mequiv{}  g  x2
By
Latex:
((Assert  ||x1||  =  r0  BY
                (BLemma  `rleq\_antisymmetry`  THEN  Auto))
  THEN  (RWO    "real-vec-norm-is-0"  (-1)  THENA  Auto)
  )
Home
Index