---

Step * 1 1 1 1 1 1 1 2 1 of Lemma continuous-abs-subtype

.....wf..... 
1. I : Interval
2. f : I ⟶ℝ
3. mc : f[x] continuous for x ∈ I
4. λm,n. rmin(mc m n;mc m n) ∈ |f[x]| continuous for x ∈ I
5. m : {m:ℕ+| icompact(i-approx(I;m))} 
6. n : ℕ+
7. mc m n ∈ ℝ
8. v : |f[x]| continuous for x ∈ I
9. (λm,n. rmin(mc m n;mc m n)) = v ∈ |f[x]| continuous for x ∈ I
10. (v m n) = rmin(mc m n;mc m n) ∈ ℝ
⊢ mc m n ∈ ℝ
BY
{ (RepUR ``continuous all sq_exists`` 3
   THEN DoSubsume
   THEN Auto
   THEN ∀h:hyp. (FLemma `i-member-approx` [h] THEN Auto) ⋅) }

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  mc  :  f[x]  continuous  for  x  \mmember{}  I
4.  \mlambda{}m,n.  rmin(mc  m  n;mc  m  n)  \mmember{}  |f[x]|  continuous  for  x  \mmember{}  I
5.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\} 
6.  n  :  \mBbbN{}\msupplus{}
7.  mc  m  n  \mmember{}  \mBbbR{}
8.  v  :  |f[x]|  continuous  for  x  \mmember{}  I
9.  (\mlambda{}m,n.  rmin(mc  m  n;mc  m  n))  =  v
10.  (v  m  n)  =  rmin(mc  m  n;mc  m  n)
\mvdash{}  mc  m  n  \mmember{}  \mBbbR{}


By

---

Latex:
(RepUR  ``continuous  all  sq\_exists``  3
  THEN  DoSubsume
  THEN  Auto
  THEN  \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THEN  Auto)  \mcdot{})

---

Home Index