---

Step * of Lemma continuous-minus

∀[I:Interval]. ∀[f:I ⟶ℝ].  (f[x] continuous for x ∈ I ⇒ -(f[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 ⌜d⌝ (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. m : {m:ℕ+| icompact(i-approx(I;m))} @i
4. n : ℕ+@i
5. d : ℝ
6. r0 < d
7. r0 < d
8. x : ℝ@i
9. y : ℝ@i
10. x ∈ i-approx(I;m)@i
11. y ∈ i-approx(I;m)@i
12. |x - y| ≤ d@i
13. |f[x] - f[y]| ≤ (r1/r(n))
⊢ |-(f[x]) - -(f[y])| ≤ (r1/r(n))

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].    (f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  -(f[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{}d\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