---

Step * of Lemma continuous-const

∀[I:Interval]. ∀[a:ℝ].  a continuous for x ∈ I
BY
{ (Auto THEN (D 0 THEN Auto) THEN With ⌜r(10000000)⌝ (D 0)⋅ THEN Auto) }

1
1. I : Interval
2. a : ℝ
3. m : {m:ℕ+| icompact(i-approx(I;m))} 
4. n : ℕ+
5. r0 < r(10000000)
6. x : ℝ
7. y : ℝ
8. x ∈ i-approx(I;m)
9. y ∈ i-approx(I;m)
10. |x - y| ≤ r(10000000)
⊢ |a - a| ≤ (r1/r(n))

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[a:\mBbbR{}].    a  continuous  for  x  \mmember{}  I


By

---

Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  With  \mkleeneopen{}r(10000000)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index