---

Step * 1 of Lemma remove-singularity-max-mfun


1. X : Type
2. d : metric(X)
3. k : ℕ
4. λi.r0 ∈ ℝ^k
5. f : {p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X
6. z : X
7. ∃c:{c:ℝ| r0 ≤ c} 
    ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .
      ((mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
8. mcomplete(X with d)
9. g : ℝ^k ⟶ X
10. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
11. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
12. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
13. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
14. ∀x1,x2:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .  (x1 ≡ x2 ⇒ f x1 ≡ f x2)
15. x1 : ℝ^k
16. x2 : ℝ^k
17. x1 ≡ x2
18. r0 < mdist(max-metric(k);x1;λi.r0)
⊢ g x1 ≡ g x2
BY
{ ((StableCases ⌜r0 < mdist(max-metric(k);x2;λi.r0)⌝⋅ THENA Auto) THEN Try ((FLemma `not-rless` [-1] THENA Auto))) }

1
1. X : Type
2. d : metric(X)
3. k : ℕ
4. λi.r0 ∈ ℝ^k
5. f : {p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X
6. z : X
7. ∃c:{c:ℝ| r0 ≤ c} 
    ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .
      ((mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
8. mcomplete(X with d)
9. g : ℝ^k ⟶ X
10. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
11. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
12. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
13. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
14. ∀x1,x2:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .  (x1 ≡ x2 ⇒ f x1 ≡ f x2)
15. x1 : ℝ^k
16. x2 : ℝ^k
17. x1 ≡ x2
18. r0 < mdist(max-metric(k);x1;λi.r0)
19. r0 < mdist(max-metric(k);x2;λi.r0)
⊢ g x1 ≡ g x2

2
1. X : Type
2. d : metric(X)
3. k : ℕ
4. λi.r0 ∈ ℝ^k
5. f : {p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X
6. z : X
7. ∃c:{c:ℝ| r0 ≤ c} 
    ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .
      ((mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(m))) ⇒ (mdist(d;f p;z) ≤ (c/r(m))))
8. mcomplete(X with d)
9. g : ℝ^k ⟶ X
10. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
11. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
12. ∀p:ℝ^k. (req-vec(k;p;λi.r0) ⇒ g p ≡ z)
13. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f p
14. ∀x1,x2:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .  (x1 ≡ x2 ⇒ f x1 ≡ f x2)
15. x1 : ℝ^k
16. x2 : ℝ^k
17. x1 ≡ x2
18. r0 < mdist(max-metric(k);x1;λi.r0)
19. ¬(r0 < mdist(max-metric(k);x2;λi.r0))
20. mdist(max-metric(k);x2;λi.r0) ≤ r0
⊢ g x1 ≡ g x2

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  k  :  \mBbbN{}
4.  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}k
5.  f  :  \{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}    {}\mrightarrow{}  X
6.  z  :  X
7.  \mexists{}c:\{c:\mBbbR{}|  r0  \mleq{}  c\} 
        \mforall{}m:\mBbbN{}\msupplus{}.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}  .
            ((mdist(max-metric(k);p;\mlambda{}i.r0)  \mleq{}  (r(4)/r(m)))  {}\mRightarrow{}  (mdist(d;f  p;z)  \mleq{}  (c/r(m))))
8.  mcomplete(X  with  d)
9.  g  :  \mBbbR{}\^{}k  {}\mrightarrow{}  X
10.  \mforall{}p:\mBbbR{}\^{}k.  (req-vec(k;p;\mlambda{}i.r0)  {}\mRightarrow{}  g  p  \mequiv{}  z)
11.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}  .  g  p  \mequiv{}  f  p
12.  \mforall{}p:\mBbbR{}\^{}k.  (req-vec(k;p;\mlambda{}i.r0)  {}\mRightarrow{}  g  p  \mequiv{}  z)
13.  \mforall{}p:\{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}  .  g  p  \mequiv{}  f  p
14.  \mforall{}x1,x2:\{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}  .    (x1  \mequiv{}  x2  {}\mRightarrow{}  f  x1  \mequiv{}  f  x2)
15.  x1  :  \mBbbR{}\^{}k
16.  x2  :  \mBbbR{}\^{}k
17.  x1  \mequiv{}  x2
18.  r0  <  mdist(max-metric(k);x1;\mlambda{}i.r0)
\mvdash{}  g  x1  \mequiv{}  g  x2


By

---

Latex:
((StableCases  \mkleeneopen{}r0  <  mdist(max-metric(k);x2;\mlambda{}i.r0)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((FLemma  `not-rless`  [-1]  THENA  Auto))
  )

---

Home Index