---

Step * of Lemma continuous-max

∀[I:Interval]. ∀[f,g:I ⟶ℝ].
  (f[x] continuous for x ∈ I ⇒ g[x] continuous for x ∈ I ⇒ rmax(f[x];g[x]) continuous for x ∈ I)
BY
{ (Auto
   THEN All (Unfold `continuous`)
   THEN Auto
   THEN ∀h:hyp. ((InstHyp [⌜m⌝;⌜n⌝] h⋅ THENA Auto) THEN Thin h THEN D -1) 
   THEN With ⌜rmin(d;d1)⌝ (D 0)⋅
   THEN Auto
   THEN Try (OnMaybeHyp 9 (\h. (FLemma `i-member-approx` [h] THEN Complete (Auto)))⋅)
   THEN EAuto 1
   THEN ∀h:hyp. ((InstHyp [⌜x⌝;⌜y⌝] h⋅
                  THENA (Auto THEN OnMaybeHyp 17 (\h. (RW (AddrC [1] (HypC h)) 0 THEN Complete (Auto)))⋅)
                  )
                 THEN Thin h
                 ) ⋅) }

1
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. m : {m:ℕ+| icompact(i-approx(I;m))} @i
5. n : ℕ+@i
6. d : ℝ
7. r0 < d
8. d1 : ℝ
9. r0 < d1
10. r0 < rmin(d;d1)
11. x : ℝ@i
12. y : ℝ@i
13. x ∈ i-approx(I;m)@i
14. y ∈ i-approx(I;m)@i
15. |x - y| ≤ rmin(d;d1)@i
16. |f[x] - f[y]| ≤ (r1/r(n))
17. |g[x] - g[y]| ≤ (r1/r(n))
⊢ |rmax(f[x];g[x]) - rmax(f[y];g[y])| ≤ (r1/r(n))

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[f,g:I  {}\mrightarrow{}\mBbbR{}].
    (f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  g[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  rmax(f[x];g[x])  continuous  for  x  \mmember{}  I)


By

---

Latex:
(Auto
  THEN  All  (Unfold  `continuous`)
  THEN  Auto
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  THEN  Thin  h  THEN  D  -1) 
  THEN  With  \mkleeneopen{}rmin(d;d1)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Try  (OnMaybeHyp  9  (\mbackslash{}h.  (FLemma  `i-member-approx`  [h]  THEN  Complete  (Auto)))\mcdot{})
  THEN  EAuto  1
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  h\mcdot{}
                                THENA  (Auto
                                              THEN  OnMaybeHyp  17  (\mbackslash{}h.  (RW  (AddrC  [1]  (HypC  h))  0  THEN  Complete  (Auto)))\mcdot{}
                                              )
                                )
                              THEN  Thin  h
                              )  \mcdot{})

---

Home Index