---

Step * of Lemma continuous-rneq

∀I:Interval. ∀f:I ⟶ℝ.  (f[x] continuous for x ∈ I ⇒ (∀a,b:{x:ℝ| x ∈ I} .  (f[a] ≠ f[b] ⇒ a ≠ b)))
BY
{ (Auto
   THEN (InstLemma `small-reciprocal-real` [|f[a] - f[b]|]⋅
         THENA (Auto
                THEN MemTypeCD
                THEN Auto
                THEN RWO "rabs-difference-lower-bound" 0
                THEN Auto
                THEN nRNorm 0
                THEN Auto
                THEN D (-1)
                THEN Auto)
         )
   THEN D (-1)
   THEN (InstLemma `i-approx-containing2` [⌜I⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN D -1) }

1
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

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.    (f[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  (\mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    (f[a]  \mneq{}  f[b]  {}\mRightarrow{}  a  \mneq{}  b)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `small-reciprocal-real`  [|f[a]  -  f[b]|]\mcdot{}
              THENA  (Auto
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  RWO  "rabs-difference-lower-bound"  0
                            THEN  Auto
                            THEN  nRNorm  0
                            THEN  Auto
                            THEN  D  (-1)
                            THEN  Auto)
              )
  THEN  D  (-1)
  THEN  (InstLemma  `i-approx-containing2`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index