---

Step * of Lemma strict-monotonic-is-locally-non-constant

∀I:Interval. ∀f:I ⟶ℝ.
  (((∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f x) < (f y)))) ∨ (∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f y) < (f x)))))
  ⇒ (∀a,b:{x:ℝ| x ∈ I} . ∀x:ℝ.  locally-non-constant(f;a;b;x)))
BY
{ Auto }

1
1. I : Interval
2. f : I ⟶ℝ
3. (∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f x) < (f y)))) ∨ (∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f y) < (f x))))
4. a : {x:ℝ| x ∈ I} 
5. b : {x:ℝ| x ∈ I} 
6. x : ℝ
⊢ locally-non-constant(f;a;b;x)

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    (((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  <  y)  {}\mRightarrow{}  ((f  x)  <  (f  y))))
    \mvee{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  <  y)  {}\mRightarrow{}  ((f  y)  <  (f  x)))))
    {}\mRightarrow{}  (\mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}x:\mBbbR{}.    locally-non-constant(f;a;b;x)))


By

---

Latex:
Auto

---

Home Index