---

Step * of Lemma locally-non-constant-via-rational

∀a,b,c:ℝ. ∀f:[a, b] ⟶ℝ.
  (f[x] continuous for x ∈ [a, b] ⇒ locally-non-constant(f;a;b;c) ⇒ locally-non-constant-rational(f;a;b;c))
BY
{ (Auto
   THEN UnfoldTopAb (-1)
   THEN UnfoldTopAb 0
   THEN RepeatFor 5 ((ParallelLast' THENA Auto))
   THEN ExRepD
   THEN ((With ⌜1⌝ (D 5)⋅ THENM RepUR ``i-approx`` -1) THENA (Auto THEN RepUR ``i-approx`` 0 THEN EAuto 2))
   THEN D -2) }

1
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. f : [a, b] ⟶ℝ
5. u : ℝ
6. v : ℝ
7. a ≤ u
8. u < v
9. v ≤ b
10. z : ℝ
11. u ≤ z
12. z ≤ v
13. f(z) < c
14. ∀n:ℕ+
      (∃d:{ℝ| ((r0 < d)
              ∧ (∀x,y:ℝ.
                   (((a ≤ x) ∧ (x ≤ b)) ⇒ ((a ≤ y) ∧ (y ≤ b)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))})
⊢ ∃n:ℕ+. ∃z:ℤ. ((u ≤ (r(z))/n) ∧ ((r(z))/n ≤ v) ∧ f((r(z))/n) ≠ c)

2
1. a : ℝ
2. b : ℝ
3. c : ℝ
4. f : [a, b] ⟶ℝ
5. u : ℝ
6. v : ℝ
7. a ≤ u
8. u < v
9. v ≤ b
10. z : ℝ
11. u ≤ z
12. z ≤ v
13. c < f(z)
14. ∀n:ℕ+
      (∃d:{ℝ| ((r0 < d)
              ∧ (∀x,y:ℝ.
                   (((a ≤ x) ∧ (x ≤ b)) ⇒ ((a ≤ y) ∧ (y ≤ b)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))})
⊢ ∃n:ℕ+. ∃z:ℤ. ((u ≤ (r(z))/n) ∧ ((r(z))/n ≤ v) ∧ f((r(z))/n) ≠ c)

---

Latex:

---

Latex:
\mforall{}a,b,c:\mBbbR{}.  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.
    (f[x]  continuous  for  x  \mmember{}  [a,  b]
    {}\mRightarrow{}  locally-non-constant(f;a;b;c)
    {}\mRightarrow{}  locally-non-constant-rational(f;a;b;c))


By

---

Latex:
(Auto
  THEN  UnfoldTopAb  (-1)
  THEN  UnfoldTopAb  0
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
  THEN  ExRepD
  THEN  ((With  \mkleeneopen{}1\mkleeneclose{}  (D  5)\mcdot{}  THENM  RepUR  ``i-approx``  -1)
              THENA  (Auto  THEN  RepUR  ``i-approx``  0  THEN  EAuto  2)
              )
  THEN  D  -2)

---

Home Index