---

Step * 1 of Lemma continuous-rneq


1. I : Interval@i
2. f : I ⟶ℝ@i
3. f[x] continuous for x ∈ I@i
4. a : {x:ℝ| x ∈ I} @i
5. b : {x:ℝ| x ∈ I} @i
6. f[a] ≠ f[b]@i
7. k : ℕ+
8. (r1/r(k)) < |f[a] - f[b]|
9. n : ℕ+
10. (a ∈ i-approx(I;n)) ∧ (b ∈ i-approx(I;n))
⊢ a ≠ b
BY
{ ((With ⌜n⌝ (D 3)⋅ THENA (D (-1) THEN FLemma `i-approx-compact` [-1] THEN Auto))
   THEN (With ⌜k⌝ (D (-1))⋅ THENA Auto)
   THEN D -1
   THEN (UnhideSqStableHyp (-1) THENA (Auto THEN ∀h:hyp. (FLemma `i-member-approx` [h] THEN Auto) ))) }

1
1. I : Interval@i
2. f : I ⟶ℝ@i
3. a : {x:ℝ| x ∈ I} @i
4. b : {x:ℝ| x ∈ I} @i
5. f[a] ≠ f[b]@i
6. k : ℕ+
7. (r1/r(k)) < |f[a] - f[b]|
8. n : ℕ+
9. (a ∈ i-approx(I;n)) ∧ (b ∈ i-approx(I;n))
10. d : ℝ@i
11. (r0 < d) ∧ (∀x,y:ℝ.  ((x ∈ i-approx(I;n)) ⇒ (y ∈ i-approx(I;n)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(k)))))
⊢ a ≠ b

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  f  :  I  {}\mrightarrow{}\mBbbR{}@i
3.  f[x]  continuous  for  x  \mmember{}  I@i
4.  a  :  \{x:\mBbbR{}|  x  \mmember{}  I\}  @i
5.  b  :  \{x:\mBbbR{}|  x  \mmember{}  I\}  @i
6.  f[a]  \mneq{}  f[b]@i
7.  k  :  \mBbbN{}\msupplus{}
8.  (r1/r(k))  <  |f[a]  -  f[b]|
9.  n  :  \mBbbN{}\msupplus{}
10.  (a  \mmember{}  i-approx(I;n))  \mwedge{}  (b  \mmember{}  i-approx(I;n))
\mvdash{}  a  \mneq{}  b


By

---

Latex:
((With  \mkleeneopen{}n\mkleeneclose{}  (D  3)\mcdot{}  THENA  (D  (-1)  THEN  FLemma  `i-approx-compact`  [-1]  THEN  Auto))
  THEN  (With  \mkleeneopen{}k\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (UnhideSqStableHyp  (-1)  THENA  (Auto  THEN  \mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THEN  Auto)  )))

---

Home Index